# HG changeset patch
# User blanchet
# Date 1271429514 -7200
# Node ID 54a9c06790798e247a40b6f406430b97604f29a1
# Parent  f723348b22313758ead3986558aa2c40b0c98597
output total time taken by Sledgehammer if "verbose" is set

diff -r f723348b2231 -r 54a9c0679079 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Apr 16 16:13:49 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Apr 16 16:51:54 2010 +0200
@@ -160,14 +160,22 @@
 
 (* unregister ATP thread *)
 
-fun unregister message thread = Synchronized.change global_state
+fun unregister ({verbose, ...} : params) message thread =
+  Synchronized.change global_state
   (fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
     (case lookup_thread active thread of
-      SOME (_, _, description) =>
+      SOME (birth_time, _, description) =>
         let
           val active' = delete_thread thread active;
-          val cancelling' = (thread, (Time.now (), description)) :: cancelling;
-          val message' = description ^ "\n" ^ message;
+          val now = Time.now ()
+          val cancelling' = (thread, (now, description)) :: cancelling;
+          val message' =
+            description ^ "\n" ^ message ^
+            (if verbose then
+               "Total time: " ^ Int.toString (Time.toMilliseconds
+                                          (Time.- (now, birth_time))) ^ " ms.\n"
+             else
+               "")
           val messages' = message' :: messages;
           val store' = message' ::
             (if length store <= message_store_limit then store
@@ -190,7 +198,7 @@
     else priority ("Sledgehammer: " ^ space_implode "\n\n" msgs)
   end;
 
-fun check_thread_manager () = Synchronized.change global_state
+fun check_thread_manager params = Synchronized.change global_state
   (fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
     if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
     else let val manager = SOME (Toplevel.thread false (fn () =>
@@ -223,7 +231,7 @@
         do
           (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
             |> these
-            |> List.app (unregister "Interrupted (reached timeout)");
+            |> List.app (unregister params "Timed out.");
             print_new_messages ();
             (*give threads some time to respond to interrupt*)
             OS.Process.sleep min_wait_time)
@@ -233,7 +241,7 @@
 
 (* register ATP thread *)
 
-fun register birth_time death_time (thread, desc) =
+fun register params birth_time death_time (thread, desc) =
  (Synchronized.change global_state
     (fn {manager, timeout_heap, active, cancelling, messages, store} =>
       let
@@ -241,7 +249,7 @@
         val active' = update_thread (thread, (birth_time, death_time, desc)) active;
         val state' = make_state manager timeout_heap' active' cancelling messages store;
       in state' end);
-  check_thread_manager ());
+  check_thread_manager params);
 
 
 
@@ -336,7 +344,7 @@
 
         val _ = Toplevel.thread true (fn () =>
           let
-            val _ = register birth_time death_time (Thread.self (), desc);
+            val _ = register params birth_time death_time (Thread.self (), desc)
             val problem =
               {subgoal = i, goal = (ctxt, (facts, goal)),
                relevance_override = relevance_override, axiom_clauses = NONE,
@@ -345,7 +353,7 @@
               handle Sledgehammer_HOL_Clause.TRIVIAL =>
                   metis_line i n []
                 | ERROR msg => ("Error: " ^ msg);
-            val _ = unregister message (Thread.self ());
+            val _ = unregister params message (Thread.self ());
           in () end);
       in () end);