Module AsyncTaskQueue

val async_proofs_flags_for_workers : string list Stdlib.ref
module type Task = sig ... end

The Task module type defines an abstract message-processing queue.

type cancel_switch = bool Stdlib.ref

cancel_switch to be flipped to true by anyone to signal the task is not relevant anymore. When the STM performs an undo/edit-at, it crawls the document and flips these flags (the Qed node carries a pointer to the flag IIRC).

module MakeQueue : functor (T : Task) -> functor () sig ... end

Client-side functor. MakeQueue T creates a task queue for task T

module MakeWorker : functor (T : Task) -> functor () sig ... end

Server-side functor. MakeWorker T creates the server task dispatcher.