From 56ba2afe14a19bd0d396f89cab3ae720f2664be3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 31 Jan 2018 05:22:31 +0100 Subject: [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. --- stm/proofworkertop.ml | 2 +- stm/queryworkertop.ml | 2 +- stm/tacworkertop.ml | 2 +- stm/workerLoop.ml | 4 ++-- stm/workerLoop.mli | 2 +- 5 files changed, 6 insertions(+), 6 deletions(-) (limited to 'stm') diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml index 10b42f7e9..def60d1b9 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 a1fe50c63..928a6bfb0 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 17f90b7b1..f202fc7c5 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 704119186..d606f19bf 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 da2e6fe0c..c42b48a28 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 -- cgit v1.2.3