# 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)