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

2 files changed, 2 insertions, 0 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index d94482cebf..993ebaa705 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -56,6 +56,7 @@ let async_proofs_n_workers = ref 1
 let async_proofs_n_tacworkers = ref 2
 let async_proofs_private_flags = ref None
 let async_proofs_always_delegate = ref false
+let async_queries_always_delegate = ref false
 let async_proofs_never_reopen_branch = ref false
 let async_proofs_flags_for_workers = ref []
 let async_proofs_worker_id = ref "master"
diff --git a/lib/flags.mli b/lib/flags.mli
index e53de166d4..cfc3d5001e 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -25,6 +25,7 @@ val async_proofs_private_flags : string option ref
 val async_proofs_is_worker : unit -> bool
 val async_proofs_is_master : unit -> bool
 val async_proofs_always_delegate : bool ref
+val async_queries_always_delegate : bool ref
 val async_proofs_never_reopen_branch : bool ref
 val async_proofs_flags_for_workers : string list ref
 val async_proofs_worker_id : string ref