An attempt to reorganize further coqtop initialization into semantic units.

Incidentally moving parsing of "-batch" to the coqtop binary.

7 files changed, 81 insertions, 87 deletions

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 044ac29e92..dadf5f9f3e 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -125,7 +125,7 @@ module Make(T : Task) () = struct
                  "-async-proofs-worker-priority";
                  CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)]
         (* Options to discard: 0 arguments *)
-        | ("-emacs"|"-batch")::tl ->
+        | "-emacs"::tl ->
           set_slave_opt tl
         (* Options to discard: 1 argument *)
         | ( "-async-proofs" | "-vio2vo" | "-o"
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index e47fbf2921..b1f823cd1a 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -85,14 +85,12 @@ type coqargs_base_query =
 
 type coqargs_queries = {
   queries : coqargs_base_query list;
-  filteropts : bool;
+  filteropts : string list option;
 }
 
-type coqargs_interactive = Interactive | Batch
-
 type coqargs_main =
   | Queries of coqargs_queries
-  | Run of coqargs_interactive
+  | Run
 
 type coqargs_post = {
   memory_stat : bool;
@@ -151,12 +149,9 @@ let default_pre = {
 
 let default_queries = {
   queries = [];
-  filteropts = false;
+  filteropts = None;
 }
 
-let default_main =
-  Run Interactive
-
 let default_post = {
   memory_stat  = false;
   output_context = false;
@@ -165,7 +160,7 @@ let default_post = {
 let default = {
   config = default_config;
   pre    = default_pre;
-  main   = default_main;
+  main   = Run;
   post   = default_post;
 }
 
@@ -209,26 +204,21 @@ let set_color opts = function
   | _ ->
     error_wrong_arg ("Error: on/off/auto expected after option color")
 
-let set_batch opts =
-  { opts with main = match opts.main with
-  | Run _ -> Run Batch
-  | Queries _ as x -> x }
-
 let add_query { queries; filteropts } q =
   { queries = queries@[q]; filteropts }
 
 let set_query opts q =
   { opts with main = match opts.main with
-  | Run _ -> Queries (add_query default_queries q)
+  | Run -> Queries (add_query default_queries q)
   | Queries queries -> Queries (add_query queries q)
   }
 
 let add_filteropts { queries } =
-  { queries; filteropts = true }
+  { queries; filteropts = Some [] }
 
 let set_filteropts opts =
   { opts with main = match opts.main with
-  | Run _ -> Queries (add_filteropts default_queries)
+  | Run -> Queries (add_filteropts default_queries)
   | Queries queries -> Queries (add_filteropts queries)
   }
 
@@ -548,9 +538,6 @@ let parse_args ~help ~init arglist : t * string list =
       { oval with config = { oval.config with stm_flags = { oval.config.stm_flags with
         Stm.AsyncOpts.async_proofs_never_reopen_branch = true
       }}}
-    |"-batch" ->
-      Flags.quiet := true;
-      set_batch oval
     |"-test-mode" -> Vernacentries.test_mode := true; oval
     |"-beautify" -> Flags.beautify := true; oval
     |"-bt" -> Backtrace.record_backtrace true; oval
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 897885997c..3cbb0b109f 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -60,14 +60,12 @@ type coqargs_base_query =
 
 type coqargs_queries = {
   queries : coqargs_base_query list;
-  filteropts : bool;
+  filteropts : string list option;
 }
 
-type coqargs_interactive = Interactive | Batch
-
 type coqargs_main =
   | Queries of coqargs_queries
-  | Run of coqargs_interactive
+  | Run
 
 type coqargs_post = {
   memory_stat : bool;
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index e58b2eec3c..603d4118b5 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -30,11 +30,9 @@ let coqc_main () =
       init = coqc_init;
       parse_extra = (fun ~opts extras -> Coqcargs.parse extras, []);
     } in
-  let opts, extras =
+  let opts, copts =
     Topfmt.(in_phase ~phase:Initialization)
-      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, extras = custom_coqc.Coqtop.parse_extra ~opts extras in
+      Coqtop.init_toplevel custom_coqc 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 58dd994dcd..79b9d5d501 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -11,6 +11,9 @@
 open Pp
 open Coqargs
 
+(** This file provides generic support for Coq executables + specific
+    support for the coqtop executable *)
+
 let () = at_exit flush_all
 
 let ( / ) = Filename.concat
@@ -152,8 +155,7 @@ let print_style_tags opts =
   let () = List.iter iter tags in
   flush_all ()
 
-
-let print_queries opts extras q =
+let print_queries opts q =
   let print_query = function
     | PrintVersion -> Usage.version ()
     | PrintMachineReadableVersion -> Usage.machine_readable_version ()
@@ -162,11 +164,13 @@ let print_queries opts extras q =
     | PrintConfig -> Envars.print_config stdout Coq_config.all_src_dirs
     | PrintTags -> print_style_tags opts.config in
   List.iter print_query q.queries;
-  if q.filteropts then
+  match q.filteropts with
+  | Some extras ->
     if q.queries <> [] && extras <> [] then
       error_wrong_arg "Queries are exclusive of other arguments"
     else
       print_string (String.concat "\n" extras)
+  | None -> ()
 
 (** GC tweaking *)
 
@@ -197,35 +201,38 @@ let init_setup = function
   | None -> Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
   | Some s -> Envars.set_user_coqlib s
 
-(** Main init routine *)
-let init_toplevel ~help ~init custom_init arglist =
+let init_process () =
   (* Coq's init process, phase 1:
      OCaml parameters, basic structures, and IO
    *)
   CProfile.init_profile ();
   init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
-
-  Lib.init();
-
+  Lib.init ()
+
+let init_parse parse_extra help init_opts =
+  let opts, extras =
+    parse_args ~help:help ~init:init_opts
+      (List.tl (Array.to_list Sys.argv)) in
+  let customopts, extras = parse_extra ~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";
+    exit 1
+    end;
+  opts, customopts
+
+let init_execution opts custom_init =
   (* Coq's init process, phase 2:
      Basic Coq environment, load-path, plugins.
    *)
-  let opts, extras = parse_args ~help ~init arglist in
-  if opts.post.memory_stat then at_exit print_memory_stat;
-
   (* If we have been spawned by the Spawn module, this has to be done
    * early since the master waits us to connect back *)
   Spawned.init_channels ();
-  init_setup opts.config.coqlib;
-  (* Querying or running? *)
-  match opts.main with
-  | Queries q -> print_queries opts extras q; exit 0
-  | Run batch ->
-  (* Initialization *)
+  if opts.post.memory_stat then at_exit print_memory_stat;
   let top_lp = Coqinit.toplevel_init_load_path () in
   List.iter Loadpath.add_coq_path top_lp;
-  let opts, extras = custom_init ~opts extras in
+  custom_init ~opts;
   Mltop.init_known_plugins ();
   (* Configuration *)
   Global.set_engagement opts.config.logic.impredicative_set;
@@ -241,12 +248,7 @@ let init_toplevel ~help ~init custom_init arglist =
   inputstate opts.pre;
 
   (* This state will be shared by all the documents *)
-  Stm.init_core ();
-  batch, opts, extras
-
-let init_batch_toplevel ~help ~init custom_init args =
-  let run_mode, opts, extras = init_toplevel ~help ~init custom_init args in
-  opts, extras
+  Stm.init_core ()
 
 type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list
 
@@ -258,6 +260,18 @@ type 'a custom_toplevel =
   ; opts : Coqargs.t
   }
 
+(** Main init routine *)
+let init_toplevel custom =
+  let () = init_process () in
+  let opts, customopts = init_parse custom.parse_extra custom.help custom.opts in
+  let () = init_setup opts.config.coqlib in
+  (* Querying or running? *)
+  match opts.main with
+  | Queries q -> print_queries opts q; exit 0
+  | Run ->
+    let () = init_execution opts custom.init in
+    opts, customopts
+
 let init_document opts =
   (* Coq init process, phase 3: Stm initialization, backtracking state.
 
@@ -281,36 +295,14 @@ let init_toploop opts =
   let state = Ccompile.load_init_vernaculars opts ~state in
   state
 
-let coqtop_init ~opts =
-  init_color opts.config;
-  CoqworkmgrApi.(init !async_proofs_worker_priority);
-  Flags.if_verbose print_header ()
-
-let coqtop_parse_extra ~opts extras =
-  opts, extras
-
-let coqtop_toplevel =
-  { parse_extra = coqtop_parse_extra
-  ; help = Usage.print_usage_coqtop
-  ; init = coqtop_init
-  ; run = Coqloop.loop
-  ; opts = Coqargs.default
-  }
+type run_mode = Interactive | Batch
 
 let start_coq custom =
   let init_feeder = Feedback.add_feeder Coqloop.coqloop_feed in
   (* Init phase *)
   let run_mode, state, opts =
     try
-      let run_mode, opts, extras =
-        init_toplevel
-          ~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);
-        prerr_endline "See -help for the list of supported options";
-        exit 1
-      end;
+      let opts, run_mode = init_toplevel custom in
       let state = init_toploop opts in
       run_mode, state, opts
     with any ->
@@ -320,3 +312,25 @@ let start_coq custom =
   match run_mode with
   | Interactive -> custom.run ~opts ~state;
   | Batch -> exit 0
+
+let coqtop_init ~opts =
+  init_color opts.config;
+  CoqworkmgrApi.(init !async_proofs_worker_priority);
+  Flags.if_verbose print_header ()
+
+let coqtop_parse_extra ~opts extras =
+  let rec parse_extra run_mode = function
+  | "-batch" :: rest -> parse_extra Batch rest
+  | x :: rest ->
+    let run_mode, rest = parse_extra run_mode rest in run_mode, x :: rest
+  | [] -> run_mode, [] in
+  let run_mode, extras = parse_extra Interactive extras in
+  run_mode, extras
+
+let coqtop_toplevel =
+  { parse_extra = coqtop_parse_extra
+  ; help = Usage.print_usage_coqtop
+  ; init = coqtop_init
+  ; run = Coqloop.loop
+  ; opts = Coqargs.default
+  }
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 3f2d458407..4a86dc1b5a 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -25,19 +25,16 @@ type 'a custom_toplevel =
 
 (** [init_toplevel custom]
     Customized Coq initialization and argument parsing *)
-val init_batch_toplevel
-  :  help:(unit -> unit)
-  -> init:Coqargs.t
-  -> Coqargs.t extra_args_fn
-  -> string list
-  -> Coqargs.t * string list
+val init_toplevel : 'a custom_toplevel -> Coqargs.t * 'a
 
-val coqtop_toplevel : Coqargs.t custom_toplevel
+type run_mode = Interactive | Batch
 
-(** The Coq main module. [start custom] will parse the command line,
+(** The generic Coq main module. [start custom] will parse the command line,
    print the banner, initialize the load path, load the input state,
    load the files given on the command line, load the resource file,
    produce the output state if any, and finally will launch
    [custom.run]. *)
+val start_coq : run_mode custom_toplevel -> unit
 
-val start_coq : Coqargs.t custom_toplevel -> unit
+(** The specific characterization of the coqtop_toplevel *)
+val coqtop_toplevel : run_mode custom_toplevel
diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml
index 6d147ac308..1fcc106348 100644
--- a/toplevel/workerLoop.ml
+++ b/toplevel/workerLoop.ml
@@ -14,7 +14,7 @@ let rec parse = function
   | [] -> []
 
 let worker_parse_extra ~opts extra_args =
-  opts, parse extra_args
+  Coqtop.Interactive, parse extra_args
 
 let worker_init init ~opts =
   Flags.quiet := true;