When the stylesheet from TML to MathML generated a document without a root

[helm.git] / helm / hbugs / tutors / search_pattern_apply_tutor.ml

diff --git a/helm/hbugs/tutors/search_pattern_apply_tutor.ml b/helm/hbugs/tutors/search_pattern_apply_tutor.ml
index 531e94e0eae552df99896c198d1c62346740ce3a..4790ab88ab7620c1d89045a8873f1ced8e838c85 100644 (file)
--- a/helm/hbugs/tutors/search_pattern_apply_tutor.ml
+++ b/helm/hbugs/tutors/search_pattern_apply_tutor.ml
@@ -4,6 +4,13 @@ open Printf;;
 
 exception Empty_must;;
 
+module MQICallbacks =
+   struct
+      let log s = prerr_string s
+   end
+
+module MQI = MQueryInterpreter.Make(MQICallbacks)
+
 let broker_id = ref None
 let my_own_id = Hbugs_tutors_common.init_tutor ()
 let my_own_addr, my_own_port = "127.0.0.1", 50011
@@ -16,6 +23,7 @@ let is_authenticated id =
 
   (* thread who do the dirty work *)
 let slave (state, musing_id) =
+ try
   prerr_endline (sprintf "Hi, I'm the slave for musing %s" musing_id);
   let (proof, goal) = Hbugs_tutors_common.load_state state in
   let hint =
@@ -28,8 +36,8 @@ let slave (state, musing_id) =
         | hd::tl -> hd
       in
       let uris =
-        TacticChaser.searchPattern ~choose_must () ~status:(proof, goal)
-(*         ["cic:/pippo.con"; "cic:/pluto.con"] *)
+        TacticChaser.searchPattern
+         ~output_html:prerr_endline ~choose_must () ~status:(proof, goal)
       in
       if uris = [] then
         Sorry
@@ -41,8 +49,21 @@ let slave (state, musing_id) =
   ignore (Hbugs_messages.submit_req ~url:Hbugs_tutors_common.broker_url answer);
   prerr_endline
     (sprintf "Bye, I've completed my duties (success = %b)" (hint <> Sorry))
+ with
+  (Pxp_types.At _) as e ->
+    let rec unbox_exception =
+     function
+         Pxp_types.At (_,e) -> unbox_exception e
+      | e -> e
+    in
+     prerr_endline ("Uncaught PXP exception: " ^ Pxp_types.string_of_exn e) ;
+     (* e could be the Thread.exit exception; otherwise we will release an  *)
+     (* uncaught exception and the Pxp_types.At was already an uncaught     *)
+     (* exception ==> no additional arm                                     *)
+     raise (unbox_exception e)
 
 let hbugs_callback =
+  let ids = Hashtbl.create 17 in
   let forbidden () =
     prerr_endline "ignoring request from unauthorized broker";
     Exception ("forbidden", "")
@@ -52,15 +73,25 @@ let hbugs_callback =
       if is_authenticated broker_id then begin
         prerr_endline "received Start_musing";
         let new_musing_id = Hbugs_id_generator.new_musing_id () in
+        let id = Hbugs_deity.create slave (state, new_musing_id) in
         prerr_endline
-          (sprintf "starting a new musing (id = %s)" new_musing_id);
-        ignore (Thread.create slave (state, new_musing_id));
+         (sprintf "starting a new musing (tid = %d, id = %s)" id new_musing_id);
+        Hashtbl.add ids new_musing_id id ;
+        (*ignore (Thread.create slave (state, new_musing_id));*)
         Musing_started (my_own_id, new_musing_id)
       end else  (* broker unauthorized *)
         forbidden ();
   | Abort_musing (broker_id, musing_id) ->
+      prerr_endline "CSC: Abort_musing received" ;
       if is_authenticated broker_id then begin
-        prerr_endline "Ignoring 'Abort_musing' message ...";
+        (* prerr_endline "Ignoring 'Abort_musing' message ..."; *)
+        (try
+          Hbugs_deity.kill (Hashtbl.find ids musing_id) ;
+          Hashtbl.remove ids musing_id ;
+         with
+            Not_found
+          | Hbugs_deity.Can_t_kill _ ->
+             prerr_endline ("Can not kill slave " ^ musing_id)) ;
         Musing_aborted (my_own_id, musing_id)
       end else (* broker unauthorized *)
         forbidden ();
@@ -80,14 +111,17 @@ let callback (req: Http_types.request) outchan =
       outchan
 
 let main () =
+  let mqi_options = "" in (* default MathQL interpreter options *)
   try
     Sys.catch_break true;
     at_exit (fun () -> Hbugs_tutors_common.unregister_from_broker my_own_id);
     broker_id :=
       Some (Hbugs_tutors_common.register_to_broker
         my_own_id my_own_url "FOO" "Search_pattern_apply tutor");
+    ignore (MQI.init mqi_options) ;
     Http_daemon.start'
-      ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback
+      ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback;
+    MQI.close mqi_options
   with Sys.Break -> ()  (* exit nicely, invoking at_exit functions *)
 ;;