| | | 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.