diff options
| author | Hugo Herbelin | 2019-05-08 19:42:08 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 02:31:26 +0200 |
| commit | dd15e030be5e55d3770d27fbbc2fe0f5384f0166 (patch) | |
| tree | cff0290c690cec0acfc1ed67f90cdfba22748a36 /toplevel/coqtop.mli | |
| parent | 26b7e819746a6b36d0e22181f64549c503fe0481 (diff) | |
Adding methods help and parse_extra to custom toplevels data.
In particular, method init does not do parsing any more.
This allows for instance to let coqidetop treats itself the
"-filteropts" option.
Diffstat (limited to 'toplevel/coqtop.mli')
| -rw-r--r-- | toplevel/coqtop.mli | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index d1f0f78355..3f2d458407 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -13,24 +13,26 @@ [run] launches a custom toplevel. *) -type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list +type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list -type custom_toplevel = - { init : init_fn +type 'a custom_toplevel = + { parse_extra : 'a extra_args_fn + ; help : unit -> unit + ; init : opts:Coqargs.t -> unit ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit ; opts : Coqargs.t } -(** [init_toplevel ~help ~init custom_init arg_list] - Common Coq initialization and argument parsing *) +(** [init_toplevel custom] + Customized Coq initialization and argument parsing *) val init_batch_toplevel : help:(unit -> unit) -> init:Coqargs.t - -> init_fn + -> Coqargs.t extra_args_fn -> string list -> Coqargs.t * string list -val coqtop_toplevel : custom_toplevel +val coqtop_toplevel : Coqargs.t custom_toplevel (** The Coq main module. [start custom] will parse the command line, print the banner, initialize the load path, load the input state, @@ -38,4 +40,4 @@ val coqtop_toplevel : custom_toplevel produce the output state if any, and finally will launch [custom.run]. *) -val start_coq : custom_toplevel -> unit +val start_coq : Coqargs.t custom_toplevel -> unit |