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
.