Module AsyncTaskQueue.MakeQueue

Parameters

• T : Task

Signature

type queue

queue is the abstract queue type.

val create : int -> CoqworkmgrApi.priority -> queue

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

val destroy : queue -> unit

destroy q Deallocates q, cancelling all pending tasks.

val n_workers : queue -> int

n_workers q returns the number of workers of q

val enqueue_task : queue -> T.task -> cancel_switch:cancel_switch -> unit

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

val join : queue -> unit

join q blocks until the task queue is empty

val cancel_all : queue -> unit

cancel_all q Cancels all tasks

val cancel_worker : queue -> WorkerPool.worker_id -> unit

cancel_worker q wid cancels a particular worker wid

val set_order : queue -> (T.task -> T.task -> int) -> unit

set_order q cmp reorders q using ordering cmp

val broadcast : queue -> unit

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).

val snapshot : queue -> T.task list

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

val clear : queue -> unit

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

val with_n_workers : int -> CoqworkmgrApi.priority -> (queue -> 'a) -> 'a

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