src/HOL/Tools/atp_manager.ML

 datatype T = State of
  {timeout_heap: ThreadHeap.T,
   oldest_heap: ThreadHeap.T,
   active: (Thread.thread * (Time.time * Time.time * string)) list,
   cancelling: (Thread.thread * (Time.time * Time.time * string)) list,
-  messages: string list};
-
-fun make_state timeout_heap oldest_heap active cancelling messages =
+  messages: string list,
+  store: string list};
+
+fun make_state timeout_heap oldest_heap active cancelling messages store =
   State {timeout_heap = timeout_heap, oldest_heap = oldest_heap,
-    active = active, cancelling = cancelling, messages = messages};
-
-val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] [] []);
+    active = active, cancelling = cancelling, messages = messages, store = store};
+
+val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] [] [] []);
 
 
 (* the managing thread *)
 
 (*watches over running threads and interrupts them if required*)
 val managing_thread = ref (NONE: Thread.thread option);
 
 
 (* unregister thread *)
 
-fun unregister (success, message) thread = Synchronized.change_result state
-  (fn state as State {timeout_heap, oldest_heap, active, cancelling, messages} =>
+fun unregister (success, message) thread = Synchronized.change state
+  (fn state as State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
     (case lookup_thread active thread of
       SOME (birthtime, _, description) =>
         let
           val (group, active') =
             if success then List.partition (fn (_, (tb, _, _)) => tb = birthtime) active
             else List.partition (fn (th, _) => Thread.equal (th, thread)) active
-          (* 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
-
-          val msg = description ^ "\n" ^ message
-          val message' = "Sledgehammer: " ^ msg ^
+            fold (fn (th, (tb, _, desc)) => update_thread (th, (tb, now, desc))) group cancelling
+
+          val message' = description ^ "\n" ^ message ^
             (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))
-        in (message', make_state timeout_heap oldest_heap active' cancelling' messages') end
-    | NONE => ("", state)));
+          val store' = message' ::
+            (if length store <= message_store_limit then store
+             else #1 (chop message_store_limit store))
+        in make_state timeout_heap oldest_heap active' cancelling' (message' :: messages) store' end
+    | NONE =>state));
 
 
 (* kill excessive atp threads *)
 
 fun excessive_atps active =

 local
 
 fun kill_oldest () =
   let exception Unchanged in
     Synchronized.change_result state
-      (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
+      (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
         if ThreadHeap.is_empty oldest_heap orelse not (excessive_atps active)
         then raise Unchanged
         else
           let val ((_, oldest_thread), oldest_heap') = ThreadHeap.min_elem oldest_heap
-          in (oldest_thread, make_state timeout_heap oldest_heap' active cancelling messages) end)
-      |> (priority o unregister (false, "Interrupted (maximum number of ATPs exceeded)"))
+          in (oldest_thread, make_state timeout_heap oldest_heap' active cancelling messages store) end)
+      |> unregister (false, "Interrupted (maximum number of ATPs exceeded)")
     handle Unchanged => ()
   end;
 
 in
 
 fun kill_excessive () =
   let val State {active, ...} = Synchronized.value state
   in if excessive_atps active then (kill_oldest (); kill_excessive ()) else () end;
 
 end;
+
+fun print_new_messages () =
+  let val to_print = Synchronized.change_result state
+    (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+    (messages, make_state timeout_heap oldest_heap active cancelling [] store))  
+  in if null to_print then ()
+  else priority ("Sledgehammer: " ^ (space_implode "\n\n" to_print)) end;
 
 
 (* start a watching thread which runs forever -- only one may exist *)
 
 fun check_thread_manager () = CRITICAL (fn () =>

       fun time_limit (State {timeout_heap, ...}) =
         (case try ThreadHeap.min timeout_heap of
           NONE => SOME (Time.+ (Time.now (), max_wait_time))
         | SOME (time, _) => SOME time)
 
-      (* action: cancel find threads whose timeout is reached, and interrupt cancelling threads *)
-      fun action (State {timeout_heap, oldest_heap, active, cancelling, messages}) =
+      (* action: find threads whose timeout is reached, and interrupt cancelling threads *)
+      fun action (State {timeout_heap, oldest_heap, active, cancelling, messages, store}) =
         let val (timeout_threads, timeout_heap') =
           ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
         in
           if null timeout_threads andalso null cancelling andalso not (excessive_atps active)
           then NONE
           else
             let
               val _ = List.app (SimpleThread.interrupt o #1) cancelling
               val cancelling' = filter (Thread.isActive o #1) cancelling
-              val state' = make_state timeout_heap' oldest_heap active cancelling' messages
+              val state' = make_state timeout_heap' oldest_heap active cancelling' messages store
             in SOME (map #2 timeout_threads, state') end
         end
     in
       while true do
        (Synchronized.timed_access state time_limit action
         |> these
-        |> List.app (priority o unregister (false, "Interrupted (reached timeout)"));
+        |> List.app (unregister (false, "Interrupted (reached timeout)"));
         kill_excessive ();
+        print_new_messages ();
         (*give threads time to respond to interrupt*)
         OS.Process.sleep min_wait_time)
     end)));
 
 
 (* thread is registered here by sledgehammer *)
 
 fun register birthtime deadtime (thread, desc) =
  (check_thread_manager ();
   Synchronized.change state
-    (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
+    (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 end));
+      in make_state timeout_heap' oldest_heap' active' cancelling messages store end));
 
 
 
 (** user commands **)
 
 (* kill: move all threads to cancelling *)
 
 fun kill () = Synchronized.change state
-  (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
+  (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
     let val formerly_active = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active
-    in make_state timeout_heap oldest_heap [] (formerly_active @ cancelling) messages end);
+    in make_state timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store end);
 
 
 (* ATP info *)
 
 fun info () =

   in writeln (running ^ "\n" ^ interrupting) end;
 
 fun messages opt_limit =
   let
     val limit = the_default message_display_limit opt_limit;
-    val State {messages = msgs, ...} = Synchronized.value state
+    val State {store = msgs, ...} = Synchronized.value state
     val header = "Recent ATP messages" ^
       (if length msgs <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):");
   in writeln (space_implode "\n\n" (header :: #1 (chop limit msgs))) end;
 
 

             val result = prover (get_timeout ()) i proof_state
               handle ResHolClause.TOO_TRIVIAL
                 => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
               | ERROR msg
                 => (false, "Error: " ^ msg)
-            val _ = priority (unregister result (Thread.self ()))
+            val _ = unregister result (Thread.self ())
           in () end handle Interrupt => ())
       in () end);
 
 
 (* sledghammer for first subgoal *)