[sysinit] move initialization code from coqtop to here

We also spill (some) non-generic arguments and initialization code
out of coqargs and to coqtop, namely colors for the terminal. There are
more of these, left to later commits.

1 files changed, 18 insertions, 11 deletions

diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 9ae0d86cf1..f51df102bd 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -9,18 +9,16 @@
 (************************************************************************)
 
 (** Definition of custom toplevels.
-    [init] is used to do custom command line argument parsing.
+    [init_extra] is used to do custom initialization
     [run] launches a custom toplevel.
 *)
 
-type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list
-
 type ('a,'b) custom_toplevel =
-  { parse_extra : 'a extra_args_fn
-  ; help : Usage.specific_usage
-  ; init : 'a -> opts:Coqargs.t -> 'b
+  { parse_extra : string list -> 'a * string list
+  ; usage : Usage.specific_usage
+  ; init_extra : 'a -> Coqargs.injection_command list -> opts:Coqargs.t -> 'b
+  ; initial_args : Coqargs.t
   ; run : 'a -> opts:Coqargs.t -> 'b -> unit
-  ; opts : Coqargs.t
   }
 
 (** The generic Coq main module. [start custom] will parse the command line,
@@ -32,14 +30,23 @@ val start_coq : ('a * Stm.AsyncOpts.stm_opt,'b) custom_toplevel -> unit
 
 (** Initializer color for output *)
 
-val init_color : Coqargs.coqargs_config -> unit
+type color = [`ON | `AUTO | `EMACS | `OFF]
+
+val init_color : color -> unit
+val parse_extra_colors : string list -> color * string list
+val print_style_tags : color -> unit
 
 (** Prepare state for interactive loop *)
 
-val init_toploop : Coqargs.t -> Stm.AsyncOpts.stm_opt -> Vernac.State.t
+val init_toploop : Coqargs.t -> Stm.AsyncOpts.stm_opt -> Coqargs.injection_command list -> Vernac.State.t
 
 (** The specific characterization of the coqtop_toplevel *)
 
-type run_mode = Interactive | Batch
+type run_mode = Interactive | Batch | Query_PrintTags
+
+type toplevel_options = {
+  run_mode : run_mode;
+  color_mode : color;
+}
 
-val coqtop_toplevel : (run_mode * Stm.AsyncOpts.stm_opt,Vernac.State.t) custom_toplevel
+val coqtop_toplevel : (toplevel_options * Stm.AsyncOpts.stm_opt,Vernac.State.t) custom_toplevel