[toplevel] let toploop_init change Coq options

Toplevels may want to modify for example the Stm flags,
which after #1108 are handled in a functional way.

5 files changed, 10 insertions, 7 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 2e552b60b..c66d69c03 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -511,7 +511,7 @@ let () = Coqtop.toploop_init := (fun coq_args extra_args ->
         let args = parse extra_args in
         Flags.quiet := true;
         CoqworkmgrApi.(init High);
-        args)
+        coq_args, args)
 
 let () = Coqtop.toploop_run := loop
 
diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml
index 5445925b1..5130b019a 100644
--- a/stm/workerLoop.ml
+++ b/stm/workerLoop.ml
@@ -17,9 +17,9 @@ let rec parse = function
   | x :: rest -> x :: parse rest
   | [] -> []
 
-let loop init _coq_args extra_args =
+let loop init coq_args extra_args =
   let args = parse extra_args in
   Flags.quiet := true;
   init ();
   CoqworkmgrApi.init !async_proofs_worker_priority;
-  args
+  coq_args, args
diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli
index f02edb9bb..37ec6dacc 100644
--- a/stm/workerLoop.mli
+++ b/stm/workerLoop.mli
@@ -11,4 +11,6 @@
 (* Default priority *)
 val async_proofs_worker_priority : CoqworkmgrApi.priority ref
 
-val loop : (unit -> unit) -> Coqargs.coq_cmdopts -> string list -> string list
+val loop :
+  (unit -> unit) -> Coqargs.coq_cmdopts -> string list ->
+    Coqargs.coq_cmdopts * string list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0dabed6b7..668f9b893 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -368,7 +368,7 @@ let init_color color_mode =
 let toploop_init = ref begin fun opts x ->
   let () = init_color opts.color in
   let () = CoqworkmgrApi.init !WorkerLoop.async_proofs_worker_priority in
-  x
+  opts, x
   end
 
 let print_style_tags opts =
@@ -442,7 +442,7 @@ let init_toplevel arglist =
       let top_lp = Coqinit.toplevel_init_load_path () in
       List.iter Mltop.add_coq_path top_lp;
       Option.iter Mltop.load_ml_object_raw opts.toploop;
-      let extras = !toploop_init opts extras in
+      let opts, extras = !toploop_init opts extras in
       if not (CList.is_empty extras) then begin
         prerr_endline ("Don't know what to do with "^String.concat " " extras);
         prerr_endline "See -help for the list of supported options";
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 056279bbd..fcc569ca0 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -18,5 +18,6 @@ val init_toplevel : string list -> Vernac.State.t option * Coqargs.coq_cmdopts
 val start : unit -> unit
 
 (* For other toploops *)
-val toploop_init : (Coqargs.coq_cmdopts -> string list -> string list) ref
+val toploop_init :
+  (Coqargs.coq_cmdopts -> string list -> Coqargs.coq_cmdopts * string list) ref
 val toploop_run : (Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit) ref