From fb34aef7abe17c5471ee5f4f75af4a42bd0f7435 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 23 Feb 2006 21:34:45 +0000 Subject: [PATCH] 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 --- matita/matitaInit.ml | 10 +++++++++- matita/matitaInit.mli | 3 +++ 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml index a135fec80..19927a37e 100644 --- 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 63b84b448..c796f4854 100644 --- 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 + -- 2.39.2