| | New | (* | The thread has not been started. | *) |
| | Runnable | (* | The thread is executing. | *) |
| | Blocked | (* | The thread is blocked on a lock. | *) |
| | Waiting | (* | The thread is waiting for another thread (with no timeout). | *) |
| | Timed_waiting | (* | The thread is waiting for another thread (with a timeout). | *) |
| | Terminated | (* | The thread has terminated execution. | *) |
make g n f x
returns a new thread in group g
with name n
. The
thread will execute f x
when started; see
Thread(...).None
if the thread has terminated
its execution; see getThreadGroup(...).false
; see
interrupted(...).Java_exception
if the thread is interruptedjoin_time t m
is similar to join t
, except that the current
thread will at most wait for m
milliseconds; see
join(...).Java_exception
if m
is invalidJava_exception
if the thread is interruptedjoin_time t m n
is similar to join t
, except that the current
thread will at most wait for m
milliseconds plus n
nanoseconds; see
join(...).Java_exception
if m
or n
is invalidJava_exception
if the thread is interruptedJava_exception
if the thread has already been startedJava_exception
if the priority is invalidsleep m
waits for m
milliseconds; see
sleep(...).Java_exception
if m
is invalidJava_exception
if the thread is interruptedsleep m n
waits for m
milliseconds plus n
nanoseconds; see
sleep(...).Java_exception
if m
or n
is invalidJava_exception
if the thread is interruptedJava_exception
if the thread has already been startedwrap 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
.