queue is the abstract queue type.

create n pri will initialize the queue with n workers having priority pri. If n is 0, the queue won't spawn any process, working in a lazy local manner. not imposed by the this API

destroy q Deallocates q, cancelling all pending tasks.

n_workers q returns the number of workers of q

enqueue_task q t ~cancel_switch schedules t for execution in q. cancel_switch can be flipped to true to cancel the task.

join q blocks until the task queue is empty

cancel_all q Cancels all tasks

cancel_worker q wid cancels a particular worker wid

set_order q cmp reorders q using ordering cmp

broadcast q

This is nasty. Workers can be picky, e.g. pick tasks only when they are "on screen". Of course the screen is scrolled, and that changes the potential choice of workers to pick up a task or not.

This function wakes up the workers (the managers) that give a look (again) to the tasks in the queue.

The STM calls it when the perspective (as in PIDE) changes.

A problem here is that why task_match has access to the competence data in order to decide if the task is palatable to the worker or not... such data is local to the worker (manager). The perspective is global, so it does not quite fit this picture. This API to make all managers reconsider the tasks in the queue is the best I could came up with.

This API is crucial to Coqoon (or any other UI that invokes Stm.finish eagerly but wants the workers to "focus" on the visible part of the document).

snapshot q Takes a snapshot (non destructive but waits until all workers are enqueued)

clear q Clears q, only if the worker prool is empty

with_n_workers n pri f creates a queue, runs the function, destroys the queue. The user should call join