diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-11-26 22:27:27 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-11-27 16:06:54 +0100 |
| commit | 8c27af591cac09784d6d5bf9867fb743d5264967 (patch) | |
| tree | 3b55a0d077f394626a93b9360547b104dfdbf499 /stm/asyncTaskQueue.ml | |
| parent | f549ddbb9fae979d4b7b260316ea4754f2c28ffa (diff) | |
STM: new API async_query
When async_proofs_always_delegate is on, park proof workers and
dispatch to them queries. This flips the current way of printing
goals in PIDE base UIs: it is not the worker that prints all goals
while coomputing the states (and the dies), it is the UI that asks
for them when they are under the eyes of the user.
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions