From 6e3fc0992be7ddd841328028dec51d390fffb851 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 25 Jan 2017 01:48:41 +0100
Subject: [stm] Add common toploop for workers.

This is a small, but convenient refactoring, as it will allow common
argument parsing.
---
 stm/proofworkertop.ml |  6 +-----
 stm/queryworkertop.ml |  6 +-----
 stm/tacworkertop.ml   |  6 +-----
 stm/workerLoop.ml     | 15 +++++++++++++++
 stm/workerLoop.mli    |  9 +++++++++
 5 files changed, 27 insertions(+), 15 deletions(-)
 create mode 100644 stm/workerLoop.ml
 create mode 100644 stm/workerLoop.mli

diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
index 23538a467e..0d2f9cb747 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 fff6d55434..9d30473739 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 d5333d1077..256532c6b6 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 0000000000..56fcf8537f
--- /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 0000000000..dcbf9c88d6
--- /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
-- 
cgit v1.2.3