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.