STM: code restructured to reuse task queue for tactics

6 files changed, 15 insertions, 15 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index cefe18092b..b242bd0922 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -122,11 +122,11 @@ object
   method backtrack_last_phrase : unit task
   method initialize : unit task
   method join_document : unit task
-  method stop_worker : int -> unit task
+  method stop_worker : string -> unit task
 
   method get_n_errors : int
   method get_errors : (int * string) list
-  method get_slaves_status : int * int * string Int.Map.t
+  method get_slaves_status : int * int * string CString.Map.t
 
   method handle_failure : handle_exn_rty -> unit task
 
@@ -154,7 +154,7 @@ object(self)
   (* proofs being processed by the slaves *)
   val mutable to_process = 0
   val mutable processed = 0
-  val mutable slaves_status = Int.Map.empty
+  val mutable slaves_status = CString.Map.empty
 
   val feedbacks : feedback Queue.t = Queue.create ()
   val feedback_timer = Ideutils.mktimer ()
@@ -377,7 +377,7 @@ object(self)
           else to_process <- to_process + n
       | SlaveStatus(id,status), _ ->
           log "SlaveStatus" None;
-          slaves_status <- Int.Map.add id status slaves_status
+          slaves_status <- CString.Map.add id status slaves_status
 
       | _ ->
           if sentence <> None then Minilib.log "Unsupported feedback message"
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index 4669f016d5..d6854a3c04 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -21,11 +21,11 @@ object
   method backtrack_last_phrase : unit task
   method initialize : unit task
   method join_document : unit task
-  method stop_worker : int -> unit task
+  method stop_worker : string -> unit task
 
   method get_n_errors : int
   method get_errors : (int * string) list
-  method get_slaves_status : int * int * string Int.Map.t
+  method get_slaves_status : int * int * string CString.Map.t
 
 
   method handle_failure : Interface.handle_exn_rty -> unit task
diff --git a/ide/interface.mli b/ide/interface.mli
index 4e5e4a9cd7..4dca41a88d 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -206,7 +206,7 @@ type interp_sty = (raw * verbose) * string
 (* spiwack: [Inl] for safe and [Inr] for unsafe. *)
 type interp_rty = state_id * (string,string) Util.union
 
-type stop_worker_sty = int
+type stop_worker_sty = string
 type stop_worker_rty = unit
 
 
diff --git a/ide/session.ml b/ide/session.ml
index f42feae0c0..254c53cd62 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -26,7 +26,7 @@ class type control =
   end
 
 type errpage = (int * string) list page
-type jobpage = string Int.Map.t page
+type jobpage = string CString.Map.t page
 
 type session = {
   buffer : GText.buffer;
@@ -303,10 +303,10 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
 let create_jobpage coqtop coqops : jobpage =
   let table, access =
     make_table_widget
-      [`Int,"Worker",true; `String,"Job name",true]
+      [`String,"Worker",true; `String,"Job name",true]
       (fun columns store tp vc ->
         let row = store#get_iter tp in
-        let w = store#get ~row ~column:(find_int_col "Worker" columns) in
+        let w = store#get ~row ~column:(find_string_col "Worker" columns) in
 	let info () = Minilib.log ("Coq busy, discarding query") in
 	Coq.try_grab coqtop (coqops#stop_worker w) info
       ) in
@@ -314,7 +314,7 @@ let create_jobpage coqtop coqops : jobpage =
   let box = GPack.vbox ~homogeneous:false () in
   let () = box#pack ~expand:true table#coerce in
   let () = box#pack ~expand:false ~padding:2 tip#coerce in
-  let last_update = ref Int.Map.empty in
+  let last_update = ref CString.Map.empty in
   let callback = ref (fun _ -> ()) in
   object (self)
     inherit GObj.widget box#as_widget
@@ -324,9 +324,9 @@ let create_jobpage coqtop coqops : jobpage =
 	last_update := jobs;
 	access (fun _ store -> store#clear ());
         !callback jobs;
-	Int.Map.iter (fun id job -> access (fun columns store ->
+	CString.Map.iter (fun id job -> access (fun columns store ->
           let line = store#append () in
-          store#set line (find_int_col "Worker" columns) id;
+          store#set line (find_string_col "Worker" columns) id;
           store#set line (find_string_col "Job name" columns) job))
           jobs
       end
diff --git a/ide/session.mli b/ide/session.mli
index 925b135674..90138a0c98 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -22,7 +22,7 @@ class type control =
   end
 
 type errpage = (int * string) list page
-type jobpage = string Int.Map.t page
+type jobpage = string CString.Map.t page
 
 type session = {
   buffer : GText.buffer;
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 09626172de..3c312d3748 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -434,7 +434,7 @@ let quit_sty_t : quit_sty val_t = unit_t
 let about_sty_t : about_sty val_t = unit_t
 let init_sty_t : init_sty val_t = option_t string_t
 let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t
-let stop_worker_sty_t : stop_worker_sty val_t = int_t
+let stop_worker_sty_t : stop_worker_sty val_t = string_t
 
 let add_rty_t : add_rty val_t =
   pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t)