[toplevel] Refactor command line argument handling.

We mostly separate command line argument parsing from interpretation,
some (minor) imperative actions are still done at argument parsing
time. This tidies up the code quite a bit and allows to better follow
the complicated command line handling code.

To this effect, we group the key actions to be performed by the
toplevel into a new record type. There is still room to improve.

1 files changed, 63 insertions, 0 deletions

diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
new file mode 100644
index 000000000..8ee1a8f55
--- /dev/null
+++ b/toplevel/coqargs.mli
@@ -0,0 +1,63 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2018     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type compilation_mode = BuildVo | BuildVio | Vio2Vo
+type color = [`ON | `AUTO | `OFF]
+
+type coq_cmdopts = {
+
+  load_init   : bool;
+  load_rcfile : bool;
+  rcfile      : string option;
+
+  ml_includes : string list;
+  vo_includes : (string * Names.DirPath.t * bool) list;
+  vo_requires : (string * string option * bool option) list;
+
+  (* Fuse these two? Currently, [batch_mode] is only used to
+     distinguish coqc / coqtop in help display. *)
+  batch_mode : bool;
+  compilation_mode : compilation_mode;
+
+  toplevel_name : Names.DirPath.t;
+  toploop : string option;
+
+  compile_list: (string * bool) list;  (* bool is verbosity  *)
+  compilation_output_name : string option;
+
+  load_vernacular_list : (string * bool) list;
+
+  vio_checking: bool;
+  vio_tasks   : (int list * string) list;
+  vio_files   : string list;
+  vio_files_j : int;
+
+  color : color;
+
+  impredicative_set : Declarations.set_predicativity;
+  stm_flags   : Stm.AsyncOpts.stm_opt;
+  debug       : bool;
+  time        : bool;
+
+  filter_opts : bool;
+
+  glob_opt    : bool;
+
+  memory_stat : bool;
+  print_tags  : bool;
+  print_where : bool;
+  print_config: bool;
+  output_context : bool;
+
+  inputstate  : string option;
+  outputstate : string option;
+
+}
+
+val parse_args : string list -> coq_cmdopts * string list
+val exitcode : coq_cmdopts -> int