aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-04-17 10:12:17 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-04-19 11:32:07 +0200
commit2cf58e18f01fa379c5be3d3dddf41d8051fcc1cc (patch)
treecf41c91a05d682f323cda605066dcfa1816b4ac5
parented5ec093c216bef6629657f69d7f94256e3ec009 (diff)
[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.
-rw-r--r--ide/ide_slave.ml2
-rw-r--r--stm/workerLoop.ml4
-rw-r--r--stm/workerLoop.mli4
-rw-r--r--toplevel/coqtop.ml4
-rw-r--r--toplevel/coqtop.mli3
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