diff options
| author | Emilio Jesus Gallego Arias | 2018-01-31 05:22:31 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-02-09 23:02:59 +0100 |
| commit | 56ba2afe14a19bd0d396f89cab3ae720f2664be3 (patch) | |
| tree | 73a5ad4a3ee89559b78522c3fbc4ad14d17e0beb /stm | |
| 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 'stm')
| -rw-r--r-- | stm/proofworkertop.ml | 2 | ||||
| -rw-r--r-- | stm/queryworkertop.ml | 2 | ||||
| -rw-r--r-- | stm/tacworkertop.ml | 2 | ||||
| -rw-r--r-- | stm/workerLoop.ml | 4 | ||||
| -rw-r--r-- | stm/workerLoop.mli | 2 |
5 files changed, 6 insertions, 6 deletions
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml index 10b42f7e91..def60d1b99 100644 --- a/stm/proofworkertop.ml +++ b/stm/proofworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ _ -> W.main_loop ()) diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml index a1fe50c63e..928a6bfb05 100644 --- a/stm/queryworkertop.ml +++ b/stm/queryworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ _ -> W.main_loop ()) diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml index 17f90b7b15..f202fc7c55 100644 --- a/stm/tacworkertop.ml +++ b/stm/tacworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ _ -> W.main_loop ()) diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml index 7041191869..d606f19bff 100644 --- a/stm/workerLoop.ml +++ b/stm/workerLoop.ml @@ -15,8 +15,8 @@ let rec parse = function | x :: rest -> x :: parse rest | [] -> [] -let loop init args = - let args = parse args in +let loop init _coq_args extra_args = + let args = parse extra_args in Flags.quiet := true; init (); CoqworkmgrApi.init !async_proofs_worker_priority; diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli index da2e6fe0cc..c42b48a287 100644 --- a/stm/workerLoop.mli +++ b/stm/workerLoop.mli @@ -9,4 +9,4 @@ (* Default priority *) val async_proofs_worker_priority : CoqworkmgrApi.priority ref -val loop : (unit -> unit) -> string list -> string list +val loop : (unit -> unit) -> Coqargs.coq_cmdopts -> string list -> string list |