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

diff --git a/helm/hbugs/tutors/hbugs_tutors_common.ml b/helm/hbugs/tutors/hbugs_tutors_common.ml
index f00b17bc0..dca58766a 100644
--- a/helm/hbugs/tutors/hbugs_tutors_common.ml
+++ b/helm/hbugs/tutors/hbugs_tutors_common.ml
@@ -30,6 +30,7 @@ open Hbugs_types;;
 open Printf;;
 
 let broker_url = "localhost:49081/act";;
+let dump_environment_on_exit = false;;
 
 let init_tutor = Hbugs_id_generator.new_tutor_id;;
 
@@ -78,7 +79,7 @@ let typecheck_loaded_proof metasenv bo ty =
 type xml_kind = Body | Type;;
 let mk_dtdname ~ask_dtd_to_the_getter dtd =
  if ask_dtd_to_the_getter then
-  Configuration.getter_url ^ "getdtd?uri=" ^ dtd
+  Helm_registry.get "getter.url" ^ "getdtd?uri=" ^ dtd
  else
   "http://mowgli.cs.unibo.it/dtd/" ^ dtd
 ;;  
@@ -138,6 +139,7 @@ module type HbugsTutorDescription =
     val hint: hint
     val hint_type: hint_type
     val description: string
+    val environment_file: string
   end
 
 module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor =
@@ -171,24 +173,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 (_, reason) ->
+                prerr_endline (sprintf "Unable to kill slave: %s" 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 ();
@@ -207,13 +226,34 @@ module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor =
             (Exception ("parse_error", reason)))
           outchan
 
+    let restore_environment () =
+      let ic = open_in Dsc.environment_file in
+      prerr_endline "Restoring environment ...";
+      CicEnvironment.restore_from_channel
+        ~callback:(fun uri -> prerr_endline uri) ic;
+      prerr_endline "... done!";
+      close_in ic
+
+    let dump_environment () =
+      let oc = open_out Dsc.environment_file in
+      prerr_endline "Dumping environment ...";
+      CicEnvironment.dump_to_channel
+        ~callback:(fun uri -> prerr_endline uri) oc;
+      prerr_endline "... done!";
+      close_out oc
+
     let main () =
       try
         Sys.catch_break true;
-        at_exit (fun () -> unregister_from_broker my_own_id);
+        at_exit (fun () ->
+          if dump_environment_on_exit then
+            dump_environment ();
+          unregister_from_broker my_own_id);
         broker_id :=
           Some (register_to_broker
             my_own_id my_own_url Dsc.hint_type Dsc.description);
+        if Sys.file_exists Dsc.environment_file then
+          restore_environment ();
         Http_daemon.start'
           ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback
       with Sys.Break -> ()  (* exit nicely, invoking at_exit functions *)