diff options
| author | Enrico Tassi | 2014-11-26 19:05:38 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-11-27 16:06:54 +0100 |
| commit | f549ddbb9fae979d4b7b260316ea4754f2c28ffa (patch) | |
| tree | 12e254fbf260fc8c8844a7de74848816b00fdc82 /kernel/nativecode.ml | |
| parent | 5f7234edcf0a6bef995c8d1dc31f679799a98557 (diff) | |
AsyncTaskQueue: API to park a worker
Generalize the old model by letting one park a worker and
by letting the (parked) worker be picky about the tasks it
picks up.
The use of that is the following: a proof worker, while performing
its "main" task (building a proof term) computes all the intermediate
states but returns only its main result. One can ask the worker
to hang around, and react to special tasks, like printing the
goals of an intermediate state.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions
