aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.mli
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-01-31 05:22:31 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-02-09 23:02:59 +0100
commit56ba2afe14a19bd0d396f89cab3ae720f2664be3 (patch)
tree73a5ad4a3ee89559b78522c3fbc4ad14d17e0beb /toplevel/coqtop.mli
parent1222bc9e677c14884dd7c0f475003f01eb5fb1b1 (diff)
[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.
Diffstat (limited to 'toplevel/coqtop.mli')
-rw-r--r--toplevel/coqtop.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 5b9494eaa..4d625a03d 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -11,7 +11,7 @@
state, load the files given on the command line, load the resource file,
produce the output state if any, and finally will launch [Coqloop.loop]. *)
-val init_toplevel : string list -> (Stm.doc * Stateid.t) option
+val init_toplevel : string list -> (Stm.doc * Stateid.t) option * Coqargs.coq_cmdopts
val start : unit -> unit
@@ -19,6 +19,6 @@ val start : unit -> unit
val drop_last_doc : Stm.doc option ref
(* For other toploops *)
-val toploop_init : (string list -> string list) ref
-val toploop_run : (Stm.doc -> unit) ref
+val toploop_init : (Coqargs.coq_cmdopts -> string list -> string list) ref
+val toploop_run : (Coqargs.coq_cmdopts -> Stm.doc -> unit) ref