[toplevel] Allow to specify default options.

In some cases, toplevel ML clients may want to modify the default set
of flags that is passed to the main initalization routine. This is for
example useful for `idetop` to suppress some undesired printing at
startup.

I would say that clients ought to have more control, but I do expect
that PRs such as #8690 will help providing a better separation thus a
mode orthogonal API.

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 15411d55d0..202390e912 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -90,7 +90,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;
@@ -137,6 +137,8 @@ let init_args = {
 
   print_emacs = false;
 
+  (* Quiet / verbosity options should be here *)
+
   inputstate  = None;
   outputstate = None;
 }
@@ -161,6 +163,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 }
@@ -320,7 +323,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
@@ -595,5 +598,5 @@ 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 b709788dde..f7801fb069 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -62,10 +62,15 @@ 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
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 66af7f7cdf..fcc4cbfd15 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -385,7 +385,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
    *)
@@ -401,7 +401,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
@@ -488,20 +488,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