poll_time s t u is similar to pool s, except that the current
thread will at most wait for t (time value whose unit is u); see
poll(...).Java_exception if the thread is interruptedJava_exception if the thread is interruptedwrap obj wraps the reference obj into an option type:Some x if obj is not null;None if obj is null.unwrap obj unwraps the option obj into a bare reference:Some x is mapped to x;None is mapped to null.