Usage: bypassing a useless detour via a reference.

9 files changed, 56 insertions, 52 deletions

diff --git a/ide/idetop.ml b/ide/idetop.ml
index eb76951b44..02682e2ee9 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -552,11 +552,15 @@ let rec parse = function
        x :: parse rest
   | [] -> []
 
-let () = Usage.add_to_usage "coqidetop" "" "\n\
+let coqidetop_specific_usage = Usage.{
+  executable_name = "coqidetop";
+  extra_args = "";
+  extra_options = "\n\
 coqidetop specific options:\n\
 \n  --xml_formatinclude dir           (idem)\
 \n  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format\
 \n  --help-XML-protocol    print documentation of the Coq XML protocol\n"
+}
 
 let islave_parse ~opts extra_args =
   let open Coqtop in
@@ -582,7 +586,7 @@ let () =
   let open Coqtop in
   let custom = {
       parse_extra = islave_parse ;
-      help = Usage.print_usage "coqidetop";
+      help = coqidetop_specific_usage;
       init = islave_init;
       run = loop;
       opts = islave_default_opts } in
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index b07639511c..eb0331d95e 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -81,7 +81,7 @@ type coqargs_pre = {
 type coqargs_query =
   | PrintTags | PrintWhere | PrintConfig
   | PrintVersion | PrintMachineReadableVersion
-  | PrintHelp of (out_channel -> unit)
+  | PrintHelp of Usage.specific_usage
 
 type coqargs_main =
   | Queries of coqargs_query list
@@ -281,27 +281,9 @@ let parse_option_set opt =
     let v = String.sub opt (eqi+1) (len - eqi - 1) in
     to_opt_key (String.sub opt 0 eqi), Some v
 
-(*s Parsing of the command line.
-    We no longer use [Arg.parse], in order to use share [Usage.print_usage]
-    between coqtop and coqc. *)
-
-let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesystem"
-    (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned")
-
-exception NoCoqLib
-
-(* Is this still useful for displaying help? *)
-let usage help =
-  begin
-    try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib)
-    with NoCoqLib -> usage_no_coqlib ()
-  end;
-  let lp = Coqinit.toplevel_init_load_path () in
-  (* Necessary for finding the toplevels below *)
-  List.iter Loadpath.add_coq_path lp;
-  help
-
 (* Main parsing routine *)
+(*s Parsing of the command line *)
+
 let parse_args ~help ~init arglist : t * string list =
   let args = ref arglist in
   let extras = ref [] in
@@ -555,8 +537,7 @@ let parse_args ~help ~init arglist : t * string list =
     |"-type-in-type" -> set_type_in_type (); oval
     |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false)
     |"-where" -> set_query oval PrintWhere
-    |"-h"|"-H"|"-?"|"-help"|"--help" ->
-     set_query oval (PrintHelp (fun co -> usage (help co)))
+    |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help)
     |"-v"|"--version" -> set_query oval PrintVersion
     |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion
 
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 46220cd1d8..e414888861 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -56,7 +56,7 @@ type coqargs_pre = {
 type coqargs_query =
   | PrintTags | PrintWhere | PrintConfig
   | PrintVersion | PrintMachineReadableVersion
-  | PrintHelp of (out_channel -> unit)
+  | PrintHelp of Usage.specific_usage
 
 type coqargs_main =
   | Queries of coqargs_query list
@@ -77,7 +77,7 @@ type t = {
 (* Default options *)
 val default : t
 
-val parse_args : help:(out_channel -> unit) -> init:t -> string list -> t * string list
+val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * string list
 val error_wrong_arg : string -> unit
 
 val require_libs : t -> (string * string option * bool option) list
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index c905eff646..5678acb2b1 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -19,7 +19,10 @@ let coqc_init _copts ~opts =
   Coqtop.init_color opts.Coqargs.config;
   if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob ()
 
-let () = Usage.add_to_usage "coqc" "file..." "\n\
+let coqc_specific_usage = Usage.{
+  executable_name = "coqc";
+  extra_args = "file...";
+  extra_options = "\n\
 coqc specific options:\
 \n  -o f.vo                use f.vo as the output file name\
 \n  -verbose               compile and output the input file\
@@ -33,6 +36,7 @@ coqc specific options:\
 \n  -vio2vo                [see manual]\
 \n  -check-vio-tasks       [see manual]\
 \n"
+}
 
 let coqc_main copts ~opts =
   Topfmt.(in_phase ~phase:CompilationPhase)
@@ -68,7 +72,7 @@ let coqc_run copts ~opts () =
 
 let custom_coqc = Coqtop.{
   parse_extra = (fun ~opts extras -> Coqcargs.parse extras, []);
-  help = Usage.print_usage "coqc";
+  help = coqc_specific_usage;
   init = coqc_init;
   run = coqc_run;
   opts = Coqargs.default;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 5194c7a128..f09d202edf 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -159,7 +159,7 @@ let print_query opts = function
   | PrintVersion -> Usage.version ()
   | PrintMachineReadableVersion -> Usage.machine_readable_version ()
   | PrintWhere -> print_endline (Envars.coqlib ())
-  | PrintHelp f -> f stderr
+  | PrintHelp h -> Usage.print_usage stderr h
   | PrintConfig -> Envars.print_config stdout Coq_config.all_src_dirs
   | PrintTags -> print_style_tags opts.config
 
@@ -246,7 +246,7 @@ type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list
 
 type ('a,'b) custom_toplevel =
   { parse_extra : 'a extra_args_fn
-  ; help : out_channel -> unit
+  ; help : Usage.specific_usage
   ; init : 'a -> opts:Coqargs.t -> 'b
   ; run : 'a -> opts:Coqargs.t -> 'b -> unit
   ; opts : Coqargs.t
@@ -324,14 +324,18 @@ let coqtop_run run_mode ~opts state =
   | Interactive -> Coqloop.loop ~opts ~state;
   | Batch -> exit 0
 
-let () = Usage.add_to_usage "coqtop" "" "\n\
+let coqtop_specific_usage = Usage.{
+  executable_name = "coqtop";
+  extra_args = "";
+  extra_options = "\n\
 coqtop specific options:\n\
 \n  -batch                 batch mode (exits after interpretation of command line)\
 \n"
+}
 
 let coqtop_toplevel =
   { parse_extra = coqtop_parse_extra
-  ; help = Usage.print_usage "coqtop"
+  ; help = coqtop_specific_usage
   ; init = coqtop_init
   ; run = coqtop_run
   ; opts = Coqargs.default
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index af1890bee5..4fe7d538a8 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -17,7 +17,7 @@ type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list
 
 type ('a,'b) custom_toplevel =
   { parse_extra : 'a extra_args_fn
-  ; help : out_channel -> unit
+  ; help : Usage.specific_usage
   ; init : 'a -> opts:Coqargs.t -> 'b
   ; run : 'a -> opts:Coqargs.t -> 'b -> unit
   ; opts : Coqargs.t
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 636d4f8d5d..cdb2e36fbd 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -19,10 +19,6 @@ let machine_readable_version () =
 
 (* print the usage of coqtop (or coqc) on channel co *)
 
-let extra_usage = ref []
-let add_to_usage name extra text =
-  extra_usage := (name,(extra,text)) :: !extra_usage
-
 let print_usage_common co command =
   output_string co command;
   output_string co "Coq options are:\n";
@@ -103,9 +99,12 @@ let print_usage_common co command =
 
 (* print the usage *)
 
-let print_usage binfile co =
-  let extra, text =
-    try List.assoc binfile !extra_usage
-    with Not_found -> ("","") in
-  print_usage_common co ("Usage: " ^ binfile ^ " <options> " ^ extra ^ "\n\n");
-  output_string co text
+type specific_usage = {
+  executable_name : string;
+  extra_args : string;
+  extra_options : string;
+}
+
+let print_usage co { executable_name; extra_args; extra_options } =
+  print_usage_common co ("Usage: " ^ executable_name ^ " <options> " ^ extra_args ^ "\n\n");
+  output_string co extra_options
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 7d80598b7e..536cbdc6b2 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -13,10 +13,17 @@
 val version : unit -> unit
 val machine_readable_version : unit -> unit
 
-(** {6 [add_to_usage name extra_args extra_options] tell what extra
-     arguments or options to print when asking usage for command [name]. } *)
-val add_to_usage : string -> string -> string -> unit
+(** {6 extra arguments or options to print when asking usage for a
+     given executable. } *)
 
-(** {6 Prints the usage on the error output. } *)
-val print_usage : string -> out_channel -> unit
+type specific_usage = {
+  executable_name : string;
+  extra_args : string;
+  extra_options : string;
+}
+
+(** {6 Prints the generic part and specific part of usage for a
+       given executable. } *)
+
+val print_usage : out_channel -> specific_usage -> unit
 
diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml
index 3af48bad99..5f80ac475c 100644
--- a/toplevel/workerLoop.ml
+++ b/toplevel/workerLoop.ml
@@ -21,13 +21,18 @@ let worker_init init () ~opts =
   init ();
   Coqtop.init_toploop opts
 
+let worker_specific_usage name = Usage.{
+  executable_name = name;
+  extra_args = "";
+  extra_options = ("\n" ^ name ^ " specific options:\
+\n  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format\n");
+}
+
 let start ~init ~loop name =
-  let _ = Usage.add_to_usage name "" ("\n" ^ name ^ " specific options:\
-\n  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format\n") in
   let open Coqtop in
   let custom = {
     parse_extra = worker_parse_extra;
-    help = Usage.print_usage name;
+    help = worker_specific_usage name;
     opts = Coqargs.default;
     init = worker_init init;
     run = (fun () ~opts:_ _state (* why is state not used *) -> loop ());