diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-01-31 05:22:31 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-09 23:02:59 +0100 |
| commit | 56ba2afe14a19bd0d396f89cab3ae720f2664be3 (patch) | |
| tree | 73a5ad4a3ee89559b78522c3fbc4ad14d17e0beb /ide | |
| parent | 1222bc9e677c14884dd7c0f475003f01eb5fb1b1 (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 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 5f40a2242..6d1064d25 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -454,9 +454,11 @@ let slave_feeder fmt xml_oc msg = let msg_format = ref (fun () -> let margin = Option.default 72 (Topfmt.get_margin ()) in Xmlprotocol.Richpp margin -) + ) -let loop doc = +(* The loop ignores the command line arguments as the current model delegates + its handing to the toplevel container. *) +let loop _args doc = set_doc doc; init_signal_handler (); catch_break := false; @@ -504,8 +506,8 @@ let rec parse = function | x :: rest -> x :: parse rest | [] -> [] -let () = Coqtop.toploop_init := (fun args -> - let args = parse args in +let () = Coqtop.toploop_init := (fun coq_args extra_args -> + let args = parse extra_args in Flags.quiet := true; CoqworkmgrApi.(init High); args) |