# HG changeset patch
# User wenzelm
# Date 1238438967 -7200
# Node ID 09306de1d99d06f6802a0d6fc2eabe9c6491272d
# Parent  36b41d297d654aa5003777acc35aa0e3e728fa0f# Parent  ef13967f911fa4af1dc63c33b9ba270e6b6340d2
merged

diff -r ef13967f911f -r 09306de1d99d src/HOL/Tools/atp_manager.ML
--- a/src/HOL/Tools/atp_manager.ML	Mon Mar 30 20:48:01 2009 +0200
+++ b/src/HOL/Tools/atp_manager.ML	Mon Mar 30 20:49:27 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 ());