Merge PR #8826: [toplevel] Allow to specify default options.

6 files changed, 34 insertions, 17 deletions

diff --git a/ide/idetop.ml b/ide/idetop.ml
index 8cb02190e6..a2b85041e8 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -537,5 +537,5 @@ let islave_init ~opts extra_args =
 
 let () =
   let open Coqtop in
-  let custom = { init = islave_init; run = loop; } in
+  let custom = { init = islave_init; run = loop; opts = Coqargs.default_opts } in
   start_coq custom
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index b98535b201..654f4be007 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -91,7 +91,7 @@ type coq_cmdopts = {
 
 let default_toplevel = Names.(DirPath.make [Id.of_string "Top"])
 
-let init_args = {
+let default_opts = {
 
   load_init   = true;
   load_rcfile = true;
@@ -139,6 +139,8 @@ let init_args = {
 
   print_emacs = false;
 
+  (* Quiet / verbosity options should be here *)
+
   inputstate  = None;
   outputstate = None;
 }
@@ -166,6 +168,7 @@ let add_compat_require opts v =
   | Flags.Current -> add_vo_require opts "Coq.Compat.Coq89" None (Some false)
 
 let set_batch_mode opts =
+  (* XXX: This should be in the argument record *)
   Flags.quiet := true;
   System.trust_file_cache := true;
   { opts with batch_mode = true }
@@ -325,7 +328,7 @@ let usage batch =
   else Usage.print_usage_coqtop ()
 
 (* Main parsing routine *)
-let parse_args arglist : coq_cmdopts * string list =
+let parse_args init_opts arglist : coq_cmdopts * string list =
   let args = ref arglist in
   let extras = ref [] in
   let rec parse oval = match !args with
@@ -596,7 +599,7 @@ let parse_args arglist : coq_cmdopts * string list =
     parse noval
   in
   try
-    parse init_args
+    parse init_opts
   with any -> fatal_error any
 
 (******************************************************************************)
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 30f1caab12..e645b0c126 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -63,12 +63,17 @@ type coq_cmdopts = {
 
   print_emacs : bool;
 
+  (* Quiet / verbosity options should be here *)
+
   inputstate  : string option;
   outputstate : string option;
 
 }
 
-val parse_args : string list -> coq_cmdopts * string list
+(* Default options *)
+val default_opts : coq_cmdopts
+
+val parse_args : coq_cmdopts -> string list -> coq_cmdopts * string list
 val exitcode : coq_cmdopts -> int
 
 val require_libs : coq_cmdopts -> (string * string option * bool option) list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index faacbe4c80..edef741ca6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -148,7 +148,7 @@ let init_gc () =
              Gc.space_overhead = 120}
 
 (** Main init routine *)
-let init_toplevel custom_init arglist =
+let init_toplevel init_opts custom_init arglist =
   (* Coq's init process, phase 1:
      OCaml parameters, basic structures, and IO
    *)
@@ -164,7 +164,7 @@ let init_toplevel custom_init arglist =
    *)
   let res = begin
     try
-      let opts,extras = parse_args arglist in
+      let opts,extras = parse_args init_opts arglist in
       memory_stat := opts.memory_stat;
 
       (* If we have been spawned by the Spawn module, this has to be done
@@ -252,20 +252,25 @@ let init_toplevel custom_init arglist =
   Feedback.del_feeder init_feeder;
   res
 
-type custom_toplevel = {
-  init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list;
-  run : opts:coq_cmdopts -> state:Vernac.State.t -> unit;
-}
+type custom_toplevel =
+  { init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list
+  ; run : opts:coq_cmdopts -> state:Vernac.State.t -> unit
+  ; opts : Coqargs.coq_cmdopts
+  }
 
 let coqtop_init ~opts extra =
   init_color opts;
   CoqworkmgrApi.(init !async_proofs_worker_priority);
   opts, extra
 
-let coqtop_toplevel = { init = coqtop_init; run = Coqloop.loop; }
+let coqtop_toplevel =
+  { init = coqtop_init
+  ; run = Coqloop.loop
+  ; opts = Coqargs.default_opts
+  }
 
 let start_coq custom =
-  match init_toplevel custom.init (List.tl (Array.to_list Sys.argv)) with
+  match init_toplevel custom.opts custom.init (List.tl (Array.to_list Sys.argv)) with
   (* Batch mode *)
   | Some state, opts when not opts.batch_mode ->
     custom.run ~opts ~state;
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 641448f10a..c95d0aca55 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -12,10 +12,13 @@
     [init] is used to do custom command line argument parsing.
     [run] launches a custom toplevel.
 *)
-type custom_toplevel = {
-  init : opts:Coqargs.coq_cmdopts -> string list -> Coqargs.coq_cmdopts * string list;
-  run  : opts:Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit;
-}
+open Coqargs
+
+type custom_toplevel =
+  { init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list
+  ; run : opts:coq_cmdopts -> state:Vernac.State.t -> unit
+  ; opts : Coqargs.coq_cmdopts
+  }
 
 val coqtop_toplevel : custom_toplevel
 
diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml
index ee6d5e8843..e4e9a87365 100644
--- a/toplevel/workerLoop.ml
+++ b/toplevel/workerLoop.ml
@@ -23,6 +23,7 @@ let arg_init init ~opts extra_args =
 let start ~init ~loop =
   let open Coqtop in
   let custom = {
+    opts = Coqargs.default_opts;
     init = arg_init init;
     run = (fun ~opts:_ ~state:_ -> loop ());
   } in