added capability to specify externally extra command line arguments so that we

are no longer constrained to have all command line tools share the same command
line interface

diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml
index a135fec803e9b5e7028276d93d4c7186d758866d..19927a37e683e25f10c0a44e4c7fe2e7ce8a7535 100644 (file)
--- a/matita/matitaInit.ml
+++ b/matita/matitaInit.ml
@@ -126,6 +126,11 @@ let _ =
     [ "matitac", 
         sprintf "MatitaC v%s
 Usage: matitac [ OPTION ... ] FILE
+Options:"
+          BuildTimeConf.version;
+      "gragrep",
+        sprintf "Grafite Grep v%s
+Usage: gragrep [ -r ] PATH
 Options:"
           BuildTimeConf.version;
       "matita",
@@ -190,6 +195,9 @@ let usage () =
   in
   try Hashtbl.find usages usage_key with Not_found -> default_usage
 
+let extra_cmdline_specs = ref []
+let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
+
 let parse_cmdline init_status =
   if not (already_configured [CmdLine] init_status) then begin
     let includes = ref [ BuildTimeConf.stdlib_dir ] in
@@ -238,7 +246,7 @@ let parse_cmdline init_status =
           ]
         else []
       in
-      std_arg_spec @ debug_arg_spec
+      std_arg_spec @ debug_arg_spec @ !extra_cmdline_specs
     in
     let set_list ~key l =
       Helm_registry.set_list Helm_registry.of_string ~key ~value:(List.rev !l)

diff --git a/matita/matitaInit.mli b/matita/matitaInit.mli
index 63b84b448a85028d32c2f0cb111a0afa83ffd1d5..c796f48544e586277ff947a395dc20b57b0f58fa 100644 (file)
--- a/matita/matitaInit.mli
+++ b/matita/matitaInit.mli
@@ -36,3 +36,6 @@ val load_configuration_file: unit -> unit
   (** die nicely: exit with return code 1 printing usage error message *)
 val die_usage: unit -> 'a
 
+  (** add extra command line options *)
+val add_cmdline_spec: (Arg.key * Arg.spec * Arg.doc) list -> unit
+