From e6afe851f90c8a864c20fe287ee3a7d5e03c8b77 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 30 Oct 2014 17:47:07 +0100
Subject: STM: reorganize code and file names

- proofworkertop to deal with proof tasks
- tacworkertop   to deal with par: tactics
- queryworkertop to deal with queries (next commit)
---
 Makefile.common          |  2 +-
 stm/proofworkertop.ml    | 16 ++++++++++++++++
 stm/proofworkertop.mllib |  1 +
 stm/stm.ml               |  2 +-
 stm/stmworkertop.ml      | 16 ----------------
 stm/stmworkertop.mllib   |  1 -
 6 files changed, 19 insertions(+), 19 deletions(-)
 create mode 100644 stm/proofworkertop.ml
 create mode 100644 stm/proofworkertop.mllib
 delete mode 100644 stm/stmworkertop.ml
 delete mode 100644 stm/stmworkertop.mllib

diff --git a/Makefile.common b/Makefile.common
index b47a3e3224..297c046135 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -165,7 +165,7 @@ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
         parsing/parsing.cma printing/printing.cma tactics/tactics.cma \
 	stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma
 
-TOPLOOPCMA:=stm/stmworkertop.cma stm/tacworkertop.cma
+TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
 
 GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma
 
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
new file mode 100644
index 0000000000..0d1b44e494
--- /dev/null
+++ b/stm/proofworkertop.ml
@@ -0,0 +1,16 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+let () = Coqtop.toploop_init := (fun args ->
+        Flags.make_silent true;
+        Stm.slave_init_stdout ();
+        CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
+        args)
+
+let () = Coqtop.toploop_run := Stm.slave_main_loop
+
diff --git a/stm/proofworkertop.mllib b/stm/proofworkertop.mllib
new file mode 100644
index 0000000000..f9f6c22d51
--- /dev/null
+++ b/stm/proofworkertop.mllib
@@ -0,0 +1 @@
+Proofworkertop
diff --git a/stm/stm.ml b/stm/stm.ml
index 64cf9bad72..1077b8b2b3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -736,7 +736,7 @@ module Task = struct
     | RespBuiltProof of Proof_global.closed_proof_output * float
     | RespError of error
 
-  let name = "stmworker"
+  let name = "proofworker"
   let extra_env () = !async_proofs_workers_extra_env
 
   let name_of_task t = t.t_name
diff --git a/stm/stmworkertop.ml b/stm/stmworkertop.ml
deleted file mode 100644
index 0d1b44e494..0000000000
--- a/stm/stmworkertop.ml
+++ /dev/null
@@ -1,16 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-let () = Coqtop.toploop_init := (fun args ->
-        Flags.make_silent true;
-        Stm.slave_init_stdout ();
-        CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
-        args)
-
-let () = Coqtop.toploop_run := Stm.slave_main_loop
-
diff --git a/stm/stmworkertop.mllib b/stm/stmworkertop.mllib
deleted file mode 100644
index 78b54b2ea9..0000000000
--- a/stm/stmworkertop.mllib
+++ /dev/null
@@ -1 +0,0 @@
-Stmworkertop
-- 
cgit v1.2.3