Await_kernel.TerminatorSourceA termination token represents an implicit and unexpected interrupt request to be used in case of panics.
t is the type of termination tokens. Tokens become terminated by calls to Source.terminate.
is_terminated t is true if t has been terminated and false otherwise. Once is_terminated t is true it will never again become false.
check t raises Terminated if t has been terminated and does nothing otherwise.
same t1 t2 determines whether the tokens t1 and t2 are the one and the same.
is_terminatable t is true if the token has an associated source and can be terminated through it and otherwise false.
source t returns the source of the termination token This t or Null in case the token is not terminatable.
val with_ :
('a : value_or_null). (t @ local -> 'a @ unique once) @ local once ->
'a @ unique once @@ portablewith_ f creates a fresh termination token with an associated source and passes the token to f. The token is terminated when Source.terminate has been called on the source.
Panics if t still has unsignaled attached triggers when f finishes.
val with_linked :
('a : value_or_null). t @ local ->
(t @ local -> 'a @ unique once) @ local once ->
'a @ unique once @@ portablewith_linked t f creates a fresh termination token with an associated source and passes the token to f. The token is terminated when either t is terminated or Source.terminate has been called on the source.
Panics if t still has unsignaled attached triggers when f finishes.
val with_linked_multi :
('a : value_or_null). t list @ local ->
(t @ local -> 'a @ unique once) @ local once ->
'a @ unique once @@ portablewith_linked_multi ts f creates a fresh termination token with an associated source and passes the token to f. The token is canceled when any of ts are terminated or when Source.terminate has been called on the source.
Panics if t still has unsignaled attached triggers when f finishes.
add_trigger t s attaches s to the token t so that it will be signalled when t is terminated.
Returns
Terminated if t was already terminated and so s was not attached to it,Signaled if s was already signaled and so wasn't attached to t, orAttached if t was not terminated and s was not signaled and so s has been attached to t.add_trigger does not update the trigger s. In particular, a return value of Terminated tells nothing about the state of s.