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/stm.mli | |
| 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/stm.mli')
| -rw-r--r-- | stm/stm.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index 88fdf316d..5696f35c1 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -28,6 +28,8 @@ val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(located_vernac_expr -> state id) *) val query : at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> string -> unit +val async_query : + at:Stateid.t -> report_with:(Stateid.t * Feedback.route_id) -> string -> unit (* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if the requested id is the new document tip hence the document portion following |