structure IO.CancelToken : Type

Cancellation token for cooperative task cancellation: request cancellation with CancelToken.set and check for it with CancelToken.isSet. To react to cancellation without polling, register a callback with CancelToken.onSet.

This is a more flexible alternative to Task.cancel as the token can be shared between multiple tasks.

Note: the underlying Promise and the task it produces are kept private. If a future change exposes the underlying task (or the promise) publicly, the set implementation must be audited for races between resolving the promise and writing setRef: callers observing isSet = true and then waiting on the task currently rely on the order chosen in set, and that ordering interacts with the cheap Bool fast path read by the C++ runtime.

• promise : IO.Promise Unit
• setRef : IO.Ref Bool

instance IO.instNonemptyCancelToken : Nonempty CancelToken

def IO.CancelToken.new : BaseIO CancelToken

Creates a new cancellation token.

Note: cannot be called from initialize blocks because the underlying task manager is not yet running at that point. Construct lazily on first use instead.

Equations

• IO.CancelToken.new = do let promise ← IO.Promise.new let setRef ← IO.mkRef false pure { promise := promise, setRef := setRef }

def IO.CancelToken.set (tk : CancelToken) : BaseIO Unit

Activates a cancellation token. Idempotent.

Resolves the underlying promise before setting the Bool flag, so that observing isSet = true implies that any synchronously-chained onSet callbacks have already run. The reverse implication does not hold: a callback running synchronously inside set may briefly observe isSet = false.

Equations

• tk.set = do IO.Promise.resolve () (IO.CancelToken.promise✝ tk) ST.Ref.set (IO.CancelToken.setRef✝ tk) true

def IO.CancelToken.isSet (tk : CancelToken) : BaseIO Bool

Checks whether the cancellation token has been activated.

Equations

• tk.isSet = ST.Ref.get (IO.CancelToken.setRef✝ tk)

def IO.CancelToken.onSet (tk : CancelToken) (action : BaseIO Unit) : BaseIO Unit

Registers a callback to run when the cancellation token is set or dropped. The callback runs as a synchronous task dependency, so it executes inline on the thread that calls set (or on the finalizer thread if the token is dropped). If the token is already set when onSet is called, the callback runs immediately.

Equations

• tk.onSet action = BaseIO.chainTask (IO.CancelToken.promise✝ tk).result? (fun (x : Option Unit) => action) Task.Priority.default true