A classification of command line options.

A few semantic changes:
- several queries (-where, -config, ...) are accepted
- queries are exclusive of other arguments
- option -filterops is exclusive of other arguments if it contains
  another query (this allows to get rid of the "exitcode" hack)

1 files changed, 47 insertions, 28 deletions

diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 81f8983e98..897885997c 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -16,57 +16,76 @@ type native_compiler = NativeOff | NativeOn of { ondemand : bool }
 
 type option_command = OptionSet of string option | OptionUnset
 
-type t = {
+type coqargs_logic_config = {
+  impredicative_set : Declarations.set_predicativity;
+  indices_matter    : bool;
+  toplevel_name     : Stm.interactive_top;
+  allow_sprop       : bool;
+  cumulative_sprop  : bool;
+}
 
+type coqargs_config = {
+  logic       : coqargs_logic_config;
+  rcfile      : string option;
+  coqlib      : string option;
+  color       : color;
+  enable_VM   : bool;
+  native_compiler : native_compiler;
+  stm_flags   : Stm.AsyncOpts.stm_opt;
+  debug       : bool;
+  diffs_set   : bool;
+  time        : bool;
+  glob_opt    : bool;
+  print_emacs : bool;
+  set_options : (Goptions.option_name * option_command) list;
+}
+
+type coqargs_pre = {
   load_init   : bool;
   load_rcfile : bool;
-  rcfile      : string option;
 
   ml_includes : Loadpath.coq_path list;
   vo_includes : Loadpath.coq_path list;
   vo_requires : (string * string option * bool option) list;
-
-  toplevel_name : Stm.interactive_top;
+  (* None = No Import; Some false = Import; Some true = Export *)
 
   load_vernacular_list : (string * bool) list;
-  batch : bool;
-
-  color : color;
+  inputstate  : string option;
+}
 
-  impredicative_set : Declarations.set_predicativity;
-  indices_matter : bool;
-  enable_VM : bool;
-  native_compiler : native_compiler;
-  allow_sprop : bool;
-  cumulative_sprop : bool;
+type coqargs_base_query =
+  | PrintTags | PrintWhere | PrintConfig
+  | PrintVersion | PrintMachineReadableVersion
+  | PrintHelp of (unit -> unit)
 
-  set_options : (Goptions.option_name * option_command) list;
-
-  stm_flags   : Stm.AsyncOpts.stm_opt;
-  debug       : bool;
-  diffs_set   : bool;
-  time        : bool;
+type coqargs_queries = {
+  queries : coqargs_base_query list;
+  filteropts : bool;
+}
 
-  filter_opts : bool;
+type coqargs_interactive = Interactive | Batch
 
-  glob_opt    : bool;
+type coqargs_main =
+  | Queries of coqargs_queries
+  | Run of coqargs_interactive
 
+type coqargs_post = {
   memory_stat : bool;
-  print_tags  : bool;
-  print_where : bool;
-  print_config: bool;
   output_context : bool;
+}
 
-  print_emacs : bool;
-
-  inputstate  : string option;
+type t = {
+  config : coqargs_config;
+  pre : coqargs_pre;
+  main : coqargs_main;
+  post : coqargs_post;
 }
 
 (* Default options *)
 val default : t
 
 val parse_args : help:(unit -> unit) -> init:t -> string list -> t * string list
-val exitcode : t -> int
+val error_wrong_arg : string -> unit
 
 val require_libs : t -> (string * string option * bool option) list
 val build_load_path : t -> Loadpath.coq_path list