--- a/src/HOL/Tools/Sledgehammer/async_manager.ML Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Mon May 30 17:00:38 2011 +0200
@@ -111,7 +111,9 @@
Synchronized.change_result global_state
(fn {manager, timeout_heap, active, canceling, messages, store} =>
messages
- |> List.partition (fn (urgent, _) => null active orelse urgent)
+ |> List.partition
+ (fn (urgent, _) =>
+ (null active andalso null canceling) orelse urgent)
||> (fn postponed_messages =>
make_state manager timeout_heap active canceling
postponed_messages store))
@@ -156,7 +158,7 @@
do
(Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
|> these
- |> List.app (unregister (false, "Timed out.\n"));
+ |> List.app (unregister (false, "Timed out."));
print_new_messages ();
(*give threads some time to respond to interrupt*)
OS.Process.sleep min_wait_time)