diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-25 01:48:41 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-21 15:51:49 +0100 |
| commit | 6e3fc0992be7ddd841328028dec51d390fffb851 (patch) | |
| tree | 479f0c917c5678f12a948f8ba3dba731e30d08db /stm | |
| parent | 921ea3983d45051ae85b0e20bf13de2eff38e53e (diff) | |
[stm] Add common toploop for workers.
This is a small, but convenient refactoring, as it will allow common
argument parsing.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/proofworkertop.ml | 6 | ||||
| -rw-r--r-- | stm/queryworkertop.ml | 6 | ||||
| -rw-r--r-- | stm/tacworkertop.ml | 6 | ||||
| -rw-r--r-- | stm/workerLoop.ml | 15 | ||||
| -rw-r--r-- | stm/workerLoop.mli | 9 |
5 files changed, 27 insertions, 15 deletions
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml index 23538a467..0d2f9cb74 100644 --- a/stm/proofworkertop.ml +++ b/stm/proofworkertop.ml @@ -8,11 +8,7 @@ module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) -let () = Coqtop.toploop_init := (fun args -> - Flags.make_silent true; - W.init_stdout (); - CoqworkmgrApi.init !Flags.async_proofs_worker_priority; - args) +let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout let () = Coqtop.toploop_run := W.main_loop diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml index fff6d5543..9d3047373 100644 --- a/stm/queryworkertop.ml +++ b/stm/queryworkertop.ml @@ -8,11 +8,7 @@ module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) -let () = Coqtop.toploop_init := (fun args -> - Flags.make_silent true; - W.init_stdout (); - CoqworkmgrApi.init !Flags.async_proofs_worker_priority; - args) +let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout let () = Coqtop.toploop_run := W.main_loop diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml index d5333d107..256532c6b 100644 --- a/stm/tacworkertop.ml +++ b/stm/tacworkertop.ml @@ -8,11 +8,7 @@ module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) -let () = Coqtop.toploop_init := (fun args -> - Flags.make_silent true; - W.init_stdout (); - CoqworkmgrApi.init !Flags.async_proofs_worker_priority; - args) +let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout let () = Coqtop.toploop_run := W.main_loop diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml new file mode 100644 index 000000000..56fcf8537 --- /dev/null +++ b/stm/workerLoop.ml @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +let rec parse args = args + +let loop init args = + Flags.make_silent true; + init (); + CoqworkmgrApi.init !Flags.async_proofs_worker_priority; + args diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli new file mode 100644 index 000000000..dcbf9c88d --- /dev/null +++ b/stm/workerLoop.mli @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val loop : (unit -> unit) -> string list -> string list |