diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-30 18:02:45 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-31 15:54:00 +0100 |
| commit | 17147ebea482bcc9759b6cd68ed25f2416eab118 (patch) | |
| tree | f76c3f48ced370d37a39f6be5218c07d55a17594 /stm/stm.mli | |
| parent | e6afe851f90c8a864c20fe287ee3a7d5e03c8b77 (diff) | |
STM: new worker for queries
With the options -async-queries-always-delegate queries are
always delegated to a worker process (Eval, Check, ...).
Users of PIDE based UIs (in Denmark) reported that the current
behavior of processing query synchronously is rather unexpected
when one is used to get proofs processed asynchronously.
Non instantaneous queries are part of many scripts and are there
as "tests" for testing the execution of recursive functions.
A standard proof script shape in an ongoing work by Appel and Bengtson
is made of blocks like:
- recursive function definition,
- some tests,
- some proofs
And one cannot quickly jump over the tests (only the proofs).
Enclosing the queries into dummy proofs to recover a reactive UI
is just annoying. Hence this patch.
Currently CoqIDE is not able to integrate the asynchronous feedback
of the query workers into the document, hence if one passes the option
to CoqIDE one only gets a boolean out of queries (processed/error).
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 c4664a67c..57e70d24e 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -75,6 +75,8 @@ val slave_main_loop : unit -> unit val slave_init_stdout : unit -> unit val tacslave_main_loop : unit -> unit val tacslave_init_stdout : unit -> unit +val queryslave_main_loop : unit -> unit +val queryslave_init_stdout : unit -> unit val print_ast : Stateid.t -> Xml_datatype.xml |