STM: let toploop plugins specify the flags for STM workers

4 files changed, 12 insertions, 10 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 5d94270f47..92824c9f53 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -51,9 +51,10 @@ let compilation_mode = ref BuildVo
 type async_proofs = APoff | APonLazy | APonParallel of int
 let async_proofs_mode = ref APoff
 let async_proofs_n_workers = ref 1
-let async_proofs_worker_flags = ref None
+let async_proofs_private_flags = ref None
 let async_proofs_always_delegate = ref false
 let async_proofs_never_reopen_branch = ref false
+let async_proofs_flags_for_workers = ref []
 
 let async_proofs_is_worker () =
   match !async_proofs_mode with
diff --git a/lib/flags.mli b/lib/flags.mli
index 53284c6992..7f2b749b76 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -18,11 +18,11 @@ val compilation_mode : compilation_mode ref
 type async_proofs = APoff | APonLazy | APonParallel of int
 val async_proofs_mode : async_proofs ref
 val async_proofs_n_workers : int ref
-val async_proofs_worker_flags : string option ref
-
+val async_proofs_private_flags : string option ref
 val async_proofs_is_worker : unit -> bool
 val async_proofs_always_delegate : bool ref
 val async_proofs_never_reopen_branch : bool ref
+val async_proofs_flags_for_workers : string list ref
 
 val debug : bool ref
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 659cfe3c8d..4d29bbb38e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -941,10 +941,10 @@ end = struct
   let rec manage_slave ~cancel:cancel_user_req id_slave respawn =
     let ic, oc, proc =
       let rec set_slave_opt = function
-        | [] -> ["-async-proofs"; "worker"; string_of_int id_slave; "-feedback-glob"]
+        | [] -> !Flags.async_proofs_flags_for_workers @
+                ["-async-proofs"; "worker"; string_of_int id_slave]
         | ("-ideslave"|"-emacs"|"-emacs-U")::tl -> set_slave_opt tl
-        | ("-async-proofs"
-          |"-compile"
+        | ("-async-proofs" |"-toploop" |"-vi2vo" |"-compile"
           |"-compile-verbose")::_::tl -> set_slave_opt tl
         | x::tl -> x :: set_slave_opt tl in
       let args =
@@ -1513,7 +1513,7 @@ let init () =
   Backtrack.record ();
   if !Flags.async_proofs_mode = Flags.APonParallel 0 then begin
     Slaves.init ();
-    let opts = match !Flags.async_proofs_worker_flags with
+    let opts = match !Flags.async_proofs_private_flags with
       | None -> []
       | Some s -> Str.split_delim (Str.regexp ",") s in
     if String.List.mem "fallback-to-lazy-if-marshal-error=no" opts then
@@ -1920,7 +1920,8 @@ let edit_at id =
       | _, Some _, None -> assert false
       | false, Some qed_id, Some mode ->
           let tip = VCS.cur_tip () in
-          if has_failed qed_id && not !Flags.async_proofs_never_reopen_branch then reopen_branch id mode qed_id tip
+          if has_failed qed_id && not !Flags.async_proofs_never_reopen_branch
+          then reopen_branch id mode qed_id tip
           else backto id
       | true, Some qed_id, Some mode ->
           if on_cur_branch id then begin
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 73e1fb9d15..2b763b390e 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -353,8 +353,8 @@ let parse_args arglist =
         Flags.async_proofs_mode := get_async_proofs_mode opt next (next())
     |"-async-proofs-j" ->
         Flags.async_proofs_n_workers := (get_int opt (next ()))
-    |"-async-proofs-worker-flags" ->
-        Flags.async_proofs_worker_flags := Some (next ());
+    |"-async-proofs-private-flags" ->
+        Flags.async_proofs_private_flags := Some (next ());
     |"-compat" -> Flags.compat_version := get_compat_version (next ())
     |"-compile" -> add_compile false (next ())
     |"-compile-verbose" -> add_compile true (next ())