# HG changeset patch
# User blanchet
# Date 1283377240 -7200
# Node ID a02cb5717677c16cfd108e67146e89829e7d97a5
# Parent  42fcb25de0827b424fb90c4d867184270ee2b6e4
remove time information in output, since it's confusing anyway

diff -r 42fcb25de082 -r a02cb5717677 src/HOL/Tools/async_manager.ML
--- a/src/HOL/Tools/async_manager.ML	Wed Sep 01 23:10:01 2010 +0200
+++ b/src/HOL/Tools/async_manager.ML	Wed Sep 01 23:40:40 2010 +0200
@@ -9,8 +9,7 @@
 signature ASYNC_MANAGER =
 sig
   val launch :
-    string -> bool -> Time.time -> Time.time -> string -> (unit -> string)
-    -> unit
+    string -> Time.time -> Time.time -> string -> (unit -> string) -> unit
   val kill_threads : string -> string -> unit
   val running_threads : string -> string -> unit
   val thread_messages : string -> string -> int option -> unit
@@ -60,7 +59,7 @@
 
 (* unregister thread *)
 
-fun unregister verbose message thread =
+fun unregister message thread =
   Synchronized.change global_state
   (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
     (case lookup_thread active thread of
@@ -69,13 +68,7 @@
           val active' = delete_thread thread active;
           val now = Time.now ()
           val canceling' = (thread, (tool, now, desc)) :: canceling
-          val message' =
-            desc ^ "\n" ^ message ^
-            (if verbose then
-               "\nTotal time: " ^ Int.toString (Time.toMilliseconds
-                                            (Time.- (now, birth_time))) ^ " ms."
-             else
-               "")
+          val message' = desc ^ "\n" ^ message
           val messages' = (tool, message') :: messages;
           val store' = (tool, message') ::
             (if length store <= message_store_limit then store
@@ -115,7 +108,7 @@
       List.app priority (tool ^ ": " ^ hd ss :: tl ss)
     end
 
-fun check_thread_manager verbose = Synchronized.change global_state
+fun check_thread_manager () = Synchronized.change global_state
   (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
     if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
     else let val manager = SOME (Toplevel.thread false (fn () =>
@@ -148,7 +141,7 @@
         do
           (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
             |> these
-            |> List.app (unregister verbose "Timed out.\n");
+            |> List.app (unregister "Timed out.\n");
             print_new_messages ();
             (*give threads some time to respond to interrupt*)
             OS.Process.sleep min_wait_time)
@@ -158,7 +151,7 @@
 
 (* register thread *)
 
-fun register tool verbose birth_time death_time desc thread =
+fun register tool birth_time death_time desc thread =
  (Synchronized.change global_state
     (fn {manager, timeout_heap, active, canceling, messages, store} =>
       let
@@ -166,17 +159,17 @@
         val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
         val state' = make_state manager timeout_heap' active' canceling messages store;
       in state' end);
-  check_thread_manager verbose);
+  check_thread_manager ())
 
 
-fun launch tool verbose birth_time death_time desc f =
+fun launch tool birth_time death_time desc f =
   (Toplevel.thread true
        (fn () =>
            let
              val self = Thread.self ()
-             val _ = register tool verbose birth_time death_time desc self
+             val _ = register tool birth_time death_time desc self
              val message = f ()
-           in unregister verbose message self end);
+           in unregister message self end);
    ())