X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Ftutors%2Fhbugs_tutors_common.ml;h=ca3de9fed48335036e6b384796e3ea414de817a1;hb=1f9b11657c822cc762f808e0bfc5f5f2b4fb6ec7;hp=f00b17bc014998cdfa558699206df0686a4826d7;hpb=4772f0cc5107b3809128e8ed0bbef4bfffbfe1ff;p=helm.git

diff --git a/helm/hbugs/tutors/hbugs_tutors_common.ml b/helm/hbugs/tutors/hbugs_tutors_common.ml
index f00b17bc0..ca3de9fed 100644
--- a/helm/hbugs/tutors/hbugs_tutors_common.ml
+++ b/helm/hbugs/tutors/hbugs_tutors_common.ml
@@ -171,24 +171,41 @@ module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor =
         (sprintf "Bye, I've completed my duties (success = %b)" success)
 
     let hbugs_callback =
+        (* hashtbl mapping musings ids to PID of threads doing the related (dirty)
+        work *)
+      let slaves = Hashtbl.create 17 in
       let forbidden () =
         prerr_endline "ignoring request from unauthorized broker";
         Exception ("forbidden", "")
       in
-      function
+      function  (* _the_ callback *)
       | Start_musing (broker_id, state) ->
           if is_authenticated broker_id then begin
             prerr_endline "received Start_musing";
             let new_musing_id = Hbugs_id_generator.new_musing_id () in
             prerr_endline
               (sprintf "starting a new musing (id = %s)" new_musing_id);
-            ignore (Thread.create slave (state, new_musing_id));
+(*             let slave_thread = Thread.create slave (state, new_musing_id) in *)
+            let slave_thread =
+              Hbugs_deity.create slave (state, new_musing_id)
+            in
+            Hashtbl.add slaves new_musing_id slave_thread;
             Musing_started (my_own_id, new_musing_id)
           end else  (* broker unauthorized *)
             forbidden ();
       | Abort_musing (broker_id, musing_id) ->
           if is_authenticated broker_id then begin
-            prerr_endline "Ignoring 'Abort_musing' message ...";
+            (try  (* kill thread responsible for "musing_id" *)
+              let slave_thread = Hashtbl.find slaves musing_id in
+              Hbugs_deity.kill slave_thread;
+              Hashtbl.remove slaves musing_id
+            with
+            | Hbugs_deity.Can_t_kill (pid, reason) ->
+              prerr_endline (sprintf "Unable to kill slave %d: %s" pid reason)
+            | Not_found ->
+                prerr_endline (sprintf
+                  "Can't find slave corresponding to musing %s, can't kill it"
+                  musing_id));
             Musing_aborted (my_own_id, musing_id)
           end else (* broker unauthorized *)
             forbidden ();