diff options
| author | Enrico Tassi | 2021-01-06 14:19:59 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-01-27 09:45:49 +0100 |
| commit | 4c4d6cfacf92b555546055a45edc19b68245b83c (patch) | |
| tree | 3229ea96990a91d015e8059f678f67a431a1cf3b /sysinit/coqargs.mli | |
| parent | 4264aec518d5407f345c58e18e014e15e9ae96af (diff) | |
[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.
Diffstat (limited to 'sysinit/coqargs.mli')
| -rw-r--r-- | sysinit/coqargs.mli | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli index 894e0f2ef3..ebf367270d 100644 --- a/sysinit/coqargs.mli +++ b/sysinit/coqargs.mli @@ -8,14 +8,12 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -type color = [`ON | `AUTO | `EMACS | `OFF] - val default_toplevel : Names.DirPath.t type native_compiler = Coq_config.native_compiler = NativeOff | NativeOn of { ondemand : bool } -type interactive_top = TopLogical of Names.DirPath.t | TopPhysical of string +type top = TopLogical of Names.DirPath.t | TopPhysical of string type option_command = | OptionSet of string option @@ -35,14 +33,13 @@ type injection_command = type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; - toplevel_name : interactive_top; + toplevel_name : top; } type coqargs_config = { logic : coqargs_logic_config; rcfile : string option; coqlib : string option; - color : color; enable_VM : bool; native_compiler : native_compiler; native_output_dir : CUnix.physical_path; @@ -67,7 +64,7 @@ type coqargs_pre = { } type coqargs_query = - | PrintTags | PrintWhere | PrintConfig + | PrintWhere | PrintConfig | PrintVersion | PrintMachineReadableVersion | PrintHelp of Usage.specific_usage @@ -90,11 +87,13 @@ type t = { (* Default options *) val default : t -val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * string list +val parse_args : usage:Usage.specific_usage -> init:t -> string list -> t * string list val injection_commands : t -> injection_command list val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list +val dirpath_of_top : top -> Names.DirPath.t + (* Common utilities *) val get_int : opt:string -> string -> int |