# HG changeset patch
# User immler@in.tum.de
# Date 1238433076 -7200
# Node ID 36b41d297d654aa5003777acc35aa0e3e728fa0f
# Parent  787b39d499cf694b60b99d49fee5b68b322f43da
terminate watching thread

diff -r 787b39d499cf -r 36b41d297d65 src/HOL/Tools/atp_manager.ML
--- a/src/HOL/Tools/atp_manager.ML	Mon Mar 30 17:14:44 2009 +0200
+++ b/src/HOL/Tools/atp_manager.ML	Mon Mar 30 19:11:16 2009 +0200
@@ -96,6 +96,12 @@
   State {timeout_heap = timeout_heap, oldest_heap = oldest_heap,
     active = active, cancelling = cancelling, messages = messages, store = store};
 
+fun empty_state state =
+  let
+    val State {active = active, cancelling = cancelling, messages = messages, ...} =
+      Synchronized.value state
+  in (null active) andalso (null cancelling) andalso (null messages) end;
+
 val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] [] [] []);
 
 
@@ -197,7 +203,7 @@
             in SOME (map #2 timeout_threads, state') end
         end
     in
-      while true do
+      while not(empty_state state) do
        (Synchronized.timed_access state time_limit action
         |> these
         |> List.app (unregister (false, "Interrupted (reached timeout)"));
@@ -211,14 +217,14 @@
 (* thread is registered here by sledgehammer *)
 
 fun register birthtime deadtime (thread, desc) =
- (check_thread_manager ();
-  Synchronized.change state
+ (Synchronized.change state
     (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
       let
         val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap
         val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap
         val active' = update_thread (thread, (birthtime, deadtime, desc)) active
-      in make_state timeout_heap' oldest_heap' active' cancelling messages store end));
+      in make_state timeout_heap' oldest_heap' active' cancelling messages store end);
+  check_thread_manager ());