toploop plugins taken into account when printing --help (close: 3535)

E.g.

Coq options are:
  -I dir                 look for ML files in dir
  -include dir           (idem)
  [...]
  -h, --help             print this list of options

With the flag '-toploop coqidetop' these extra option are also available:
  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE

5 files changed, 31 insertions, 10 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index ef52a57741..382a0185b8 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -209,12 +209,14 @@ let init_gc () =
     between coqtop and coqc. *)
 
 let usage () =
-  if !batch_mode then
-    Usage.print_usage_coqc ()
-  else
-    Usage.print_usage_coqtop () ;
-  flush stderr ;
-  exit 1
+  Envars.set_coqlib Errors.error;
+  init_load_path ();
+  if !batch_mode then Usage.print_usage_coqc ()
+  else begin
+    Mltop.load_ml_objects_raw_rex
+      (Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$"));
+    Usage.print_usage_coqtop ()
+  end
 
 let error_missing_arg s =
   prerr_endline ("Error: extra argument expected after option "^s);
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 3c7bd8e24e..7f421c2644 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -294,6 +294,9 @@ let load_ml_object mname fname=
   init_ml_object mname
 
 let load_ml_object_raw fname = dir_ml_load (file_of_name fname)
+let load_ml_objects_raw_rex rex =
+  List.iter (fun (_,fp) -> dir_ml_load (file_of_name (Filename.basename fp)))
+    (System.where_in_path_rex !coq_mlpath_copy rex)
 
 (* Summary of declared ML Modules *)
 
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index a4ba732d26..c7435263e4 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -55,6 +55,7 @@ val add_known_module : string -> unit
 val module_is_known : string -> bool
 val load_ml_object : string -> string -> unit
 val load_ml_object_raw : string -> unit
+val load_ml_objects_raw_rex : Str.regexp -> unit
 
 (** {5 Initialization functions} *)
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 0183cfaa15..eeea7b7a60 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -14,6 +14,9 @@ let version ret =
 
 (* print the usage of coqtop (or coqc) on channel co *)
 
+let extra_usage = ref []
+let add_to_usage name text = extra_usage := (name,text) :: !extra_usage
+
 let print_usage_channel co command =
   output_string co command;
   output_string co "Coq options are:\n";
@@ -63,15 +66,22 @@ let print_usage_channel co command =
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -time                  display the time taken by each command\
 \n  -h, --help             print this list of options\
-\n  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE\
-\n"
+\n";
+  List.iter (fun (name, text) ->
+    output_string co
+     ("\nWith the flag '-toploop "^name^
+        "' these extra option are also available:\n"^
+      text^"\n"))
+    !extra_usage
 
 (* print the usage on standard error *)
 
 let print_usage = print_usage_channel stderr
 
 let print_usage_coqtop () =
-  print_usage "Usage: coqtop <options>\n\n"
+  print_usage "Usage: coqtop <options>\n\n";
+  flush stderr ;
+  exit 1
 
 let print_usage_coqc () =
   print_usage "Usage: coqc <options> <Coq options> file...\n\
@@ -80,7 +90,9 @@ let print_usage_coqc () =
 \n  -image f  specify an alternative executable for Coq\
 \n  -opt      run the native-code version of Coq\
 \n  -byte     run the bytecode version of Coq\
-\n  -t        keep temporary files\n\n"
+\n  -t        keep temporary files\n\n";
+  flush stderr ;
+  exit 1
 
 (* Print the configuration information *)
 
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 45cedf44af..aca3c0a63c 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -13,6 +13,9 @@ val version : int -> 'a
 (** {6 Prints the usage on the error output, preceeded by a user-provided message. } *)
 val print_usage : string -> unit
 
+(** {6 Enable toploop plugins to insert some text in the usage message. } *)
+val add_to_usage : string -> string -> unit
+
 (** {6 Prints the usage on the error output. } *)
 val print_usage_coqtop : unit -> unit
 val print_usage_coqc : unit -> unit