From: Claudio Sacerdoti Coen Date: Wed, 16 Apr 2003 14:12:30 +0000 (+0000) Subject: Use of Hbugs_deity for thread creation and killing. X-Git-Tag: before_refactoring~13 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=969950f7f464f94f2918a844833395920a51319c;p=helm.git Use of Hbugs_deity for thread creation and killing. --- diff --git a/helm/hbugs/tutors/search_pattern_apply_tutor.ml b/helm/hbugs/tutors/search_pattern_apply_tutor.ml index 829d86f74..0893c195f 100644 --- a/helm/hbugs/tutors/search_pattern_apply_tutor.ml +++ b/helm/hbugs/tutors/search_pattern_apply_tutor.ml @@ -16,6 +16,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 +29,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 +42,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 +66,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 ();