diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-08 11:36:44 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-09 13:11:38 +0200 |
| commit | 4d601a87b775529b7d516fa213c688b6ecf5246d (patch) | |
| tree | 0f6f2c716f3bbb8cf25032b30e4af42a223ded69 /toplevel/usage.ml | |
| parent | 938dd9ba81d0bba5a9358627405d3110fc4ee335 (diff) | |
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
Diffstat (limited to 'toplevel/usage.ml')
| -rw-r--r-- | toplevel/usage.ml | 20 |
1 files changed, 16 insertions, 4 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 0183cfaa1..eeea7b7a6 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 *) |