From 0e326def6194606d0f1e21daeb45f32e1a061c8f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 25 Dec 2014 15:51:07 +0100 Subject: Inlining Spawn.kill_if in the one place were it was actually used, thus removing the need of thread creation in the interface. --- stm/asyncTaskQueue.ml | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) (limited to 'stm/asyncTaskQueue.ml') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 917de9b52..0c40db4dc 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -108,15 +108,7 @@ module Make(T : Task) = struct let report_status ?(id = !Flags.async_proofs_worker_id) s = Pp.feedback ~state_id:Stateid.initial (Feedback.WorkerStatus(id, s)) - module Worker = Spawn.Sync(struct - let add_timeout ~sec f = - ignore(Thread.create (fun () -> - while true do - Unix.sleep sec; - if not (f ()) then Thread.exit () - done) - ()) - end) + module Worker = Spawn.Sync(struct end) module Model = struct @@ -181,10 +173,17 @@ module Make(T : Task) = struct CList.init 10 (fun _ -> Universes.new_univ_level (Global.current_dirpath ())) in - Worker.kill_if proc ~sec:1 (fun () -> - let stop = cancelled () || !(!expiration_date) in - if stop then (stop_waiting := true; TQueue.signal_destruction queue); - stop); + let rec kill_if () = + if not (Worker.is_alive proc) then () + else if cancelled () || !(!expiration_date) then + let () = stop_waiting := true in + let () = TQueue.signal_destruction queue in + Worker.kill proc + else + let () = Unix.sleep 1 in + kill_if () + in + let _ = Thread.create kill_if () in try while true do report_status ~id "Idle"; -- cgit v1.2.3