# HG changeset patch
# User immler@in.tum.de
# Date 1232490937 -3600
# Node ID 7b710756609c4d9ff38e2ad3b1ddcdba2a331da7
# Parent  93ff1bca5e152120a4f2f587f4626bc24c55a156
do not interrupt successful thread

diff -r 93ff1bca5e15 -r 7b710756609c src/HOL/Tools/atp_manager.ML
--- a/src/HOL/Tools/atp_manager.ML	Tue Jan 20 22:19:46 2009 +0100
+++ b/src/HOL/Tools/atp_manager.ML	Tue Jan 20 23:35:37 2009 +0100
@@ -114,16 +114,18 @@
           val (group, active') =
             if success then List.partition (fn (_, (tb, _, _)) => tb = birthtime) active
             else List.partition (fn (th, _) => Thread.equal (th, thread)) active
-          val others = delete_thread thread group
+          (* do not interrupt successful thread, as it needs to print out its message
+          (and terminates afterwards - see start_prover )*)
+          val group' = if success then delete_thread thread group else group
 
           val now = Time.now ()
           val cancelling' =
-            fold (fn (th, (tb, _, desc)) => update_thread (th, (tb, now, desc))) group cancelling
+            fold (fn (th, (tb, _, desc)) => update_thread (th, (tb, now, desc))) group' cancelling
 
           val msg = description ^ "\n" ^ message
           val message' = "Sledgehammer: " ^ msg ^
-            (if null others then ""
-             else "\nInterrupted " ^ string_of_int (length others) ^ " other group members")
+            (if length group <= 1 then ""
+             else "\nInterrupted " ^ string_of_int (length group - 1) ^ " other group members")
           val messages' = msg ::
             (if length messages <= message_store_limit then messages
              else #1 (chop message_store_limit messages))