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

8 files changed, 55 insertions, 19 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 6e8d298aba..5e03d27732 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -470,3 +470,5 @@ let () = Coqtop.toploop_init := (fun args ->
         args)
 
 let () = Coqtop.toploop_run := loop
+
+let () = Usage.add_to_usage "coqidetop" "  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE\n"
diff --git a/lib/system.ml b/lib/system.ml
index 511b84ab4b..a2f339b1d3 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -53,14 +53,12 @@ let all_subdirs ~unix_path:root =
   if exists_dir root then traverse root [];
   List.rev !l
 
+let rec search paths test =
+  match paths with
+  | [] -> []
+  | lpe :: rem -> test lpe @ search rem test
+
 let where_in_path ?(warn=true) path filename =
-  let rec search = function
-    | lpe :: rem ->
-	let f = Filename.concat lpe filename in
-	  if Sys.file_exists f
-	  then (lpe,f) :: search rem
-	  else search rem
-    | [] -> [] in
   let check_and_warn l = match l with
   | [] -> raise Not_found
   | (lpe, f) :: l' ->
@@ -77,7 +75,19 @@ let where_in_path ?(warn=true) path filename =
     in
     (lpe, f)
   in
-  check_and_warn (search path)
+  check_and_warn (search path (fun lpe ->
+    let f = Filename.concat lpe filename in
+    if Sys.file_exists f then [lpe,f] else []))
+
+let where_in_path_rex path rex =
+  search path (fun lpe ->
+    let files = Sys.readdir lpe in
+    CList.map_filter (fun name ->
+      try
+        ignore(Str.search_forward rex name 0);
+        Some (lpe,Filename.concat lpe name)
+      with Not_found -> None)
+      (Array.to_list files))
 
 let find_file_in_path ?(warn=true) paths filename =
   if not (Filename.is_implicit filename) then
diff --git a/lib/system.mli b/lib/system.mli
index af797121a3..e4f344f6b4 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -19,7 +19,10 @@ val exclude_search_in_dirname : string -> unit
 val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list
 val is_in_path : CUnix.load_path -> string -> bool
 val is_in_system_path : string -> bool
-val where_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
+val where_in_path :
+  ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
+val where_in_path_rex :
+  CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list
 
 val exists_dir : string -> bool
 
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