Adding methods help and parse_extra to custom toplevels data.

In particular, method init does not do parsing any more.

This allows for instance to let coqidetop treats itself the
"-filteropts" option.

4 files changed, 43 insertions, 28 deletions

diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index 7c4aded5bb..e58b2eec3c 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -21,16 +21,20 @@ let coqc_main () =
   (* Careful because init_toplevel will call Summary.init_summaries,
      thus options such as `quiet` have to be set after the main
      initialisation is run. *)
-  let coqc_init ~opts args =
+  let coqc_init ~opts =
     set_noninteractive_mode ();
-    let opts, args = Coqtop.(coqtop_toplevel.init) ~opts args in
-    opts, args
-  in
+    Coqtop.(coqtop_toplevel.init) ~opts in
+  let custom_coqc = Coqtop.{
+      coqtop_toplevel with
+      help = Usage.print_usage_coqc;
+      init = coqc_init;
+      parse_extra = (fun ~opts extras -> Coqcargs.parse extras, []);
+    } in
   let opts, extras =
     Topfmt.(in_phase ~phase:Initialization)
-      Coqtop.(init_batch_toplevel ~help:Usage.print_usage_coqc ~init:Coqargs.default coqc_init) List.(tl (Array.to_list Sys.argv)) in
+      Coqtop.(init_batch_toplevel ~help:Usage.print_usage_coqc ~init:Coqargs.default (fun ~opts extras -> coqc_init ~opts; (opts, extras))) List.(tl (Array.to_list Sys.argv)) in
 
-  let copts = Coqcargs.parse extras in
+  let copts, extras = custom_coqc.Coqtop.parse_extra ~opts extras in
 
   if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob ();
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 2f2cebe074..58dd994dcd 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -244,14 +244,16 @@ let init_toplevel ~help ~init custom_init arglist =
   Stm.init_core ();
   batch, opts, extras
 
-type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list
-
 let init_batch_toplevel ~help ~init custom_init args =
   let run_mode, opts, extras = init_toplevel ~help ~init custom_init args in
   opts, extras
 
-type custom_toplevel =
-  { init : init_fn
+type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list
+
+type 'a custom_toplevel =
+  { parse_extra : 'a extra_args_fn
+  ; help : unit -> unit
+  ; init : opts:Coqargs.t -> unit
   ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit
   ; opts : Coqargs.t
   }
@@ -279,14 +281,18 @@ let init_toploop opts =
   let state = Ccompile.load_init_vernaculars opts ~state in
   state
 
-let coqtop_init ~opts extra =
+let coqtop_init ~opts =
   init_color opts.config;
   CoqworkmgrApi.(init !async_proofs_worker_priority);
-  Flags.if_verbose print_header ();
-  opts, extra
+  Flags.if_verbose print_header ()
+
+let coqtop_parse_extra ~opts extras =
+  opts, extras
 
 let coqtop_toplevel =
-  { init = coqtop_init
+  { parse_extra = coqtop_parse_extra
+  ; help = Usage.print_usage_coqtop
+  ; init = coqtop_init
   ; run = Coqloop.loop
   ; opts = Coqargs.default
   }
@@ -298,7 +304,7 @@ let start_coq custom =
     try
       let run_mode, opts, extras =
         init_toplevel
-          ~help:Usage.print_usage_coqtop ~init:default custom.init
+          ~help:Usage.print_usage_coqtop ~init:default (fun ~opts extras -> let opts, extras = custom.parse_extra ~opts extras in custom.init ~opts; (opts, extras))
           (List.tl (Array.to_list Sys.argv)) in
       if not (CList.is_empty extras) then begin
         prerr_endline ("Don't know what to do with "^String.concat " " extras);
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index d1f0f78355..3f2d458407 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -13,24 +13,26 @@
     [run] launches a custom toplevel.
 *)
 
-type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list
+type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list
 
-type custom_toplevel =
-  { init : init_fn
+type 'a custom_toplevel =
+  { parse_extra : 'a extra_args_fn
+  ; help : unit -> unit
+  ; init : opts:Coqargs.t -> unit
   ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit
   ; opts : Coqargs.t
   }
 
-(** [init_toplevel ~help ~init custom_init arg_list]
-    Common Coq initialization and argument parsing *)
+(** [init_toplevel custom]
+    Customized Coq initialization and argument parsing *)
 val init_batch_toplevel
   :  help:(unit -> unit)
   -> init:Coqargs.t
-  -> init_fn
+  -> Coqargs.t extra_args_fn
   -> string list
   -> Coqargs.t * string list
 
-val coqtop_toplevel : custom_toplevel
+val coqtop_toplevel : Coqargs.t custom_toplevel
 
 (** The Coq main module. [start custom] will parse the command line,
    print the banner, initialize the load path, load the input state,
@@ -38,4 +40,4 @@ val coqtop_toplevel : custom_toplevel
    produce the output state if any, and finally will launch
    [custom.run]. *)
 
-val start_coq : custom_toplevel -> unit
+val start_coq : Coqargs.t custom_toplevel -> unit
diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml
index d362f9db22..6d147ac308 100644
--- a/toplevel/workerLoop.ml
+++ b/toplevel/workerLoop.ml
@@ -13,18 +13,21 @@ let rec parse = function
   | x :: rest -> x :: parse rest
   | [] -> []
 
-let arg_init init ~opts extra_args =
-  let extra_args = parse extra_args in
+let worker_parse_extra ~opts extra_args =
+  opts, parse extra_args
+
+let worker_init init ~opts =
   Flags.quiet := true;
   init ();
-  CoqworkmgrApi.(init !async_proofs_worker_priority);
-  opts, extra_args
+  CoqworkmgrApi.(init !async_proofs_worker_priority)
 
 let start ~init ~loop =
   let open Coqtop in
   let custom = {
+    parse_extra = worker_parse_extra;
+    help = (fun _ -> output_string stderr "Same options as coqtop");
     opts = Coqargs.default;
-    init = arg_init init;
+    init = worker_init init;
     run = (fun ~opts:_ ~state:_ -> loop ());
   } in
   start_coq custom