Java_exception
if the thread group is not empty, or has
already been destroyedwrap 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
.