# HG changeset patch
# User blanchet
# Date 1306767638 -7200
# Node ID 6e0cb8044734cd215deb2d0d1c7f28371c474052
# Parent  f1864c0bd165a7c4d7a6d20e8430d3f0261d7d5a
better merging of similar outputs

diff -r f1864c0bd165 -r 6e0cb8044734 src/HOL/Tools/Sledgehammer/async_manager.ML
--- 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)