diff options
| -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 |