tuned tracing;

--- a/src/Pure/Concurrent/future.ML	Sat Jul 25 00:39:05 2009 +0200
+++ b/src/Pure/Concurrent/future.ML	Sat Jul 25 00:53:47 2009 +0200
@@ -138,7 +138,7 @@
 fun count_active ws =
   fold (fn (_, active) => fn i => if active then i + 1 else i) ws 0;
 
-fun trace_active () = Multithreading.tracing 1 (fn () =>
+fun trace_active () = Multithreading.tracing 6 (fn () =>
   let
     val ws = ! workers;
     val m = string_of_int (length ws);
@@ -222,7 +222,7 @@
 fun scheduler_next () = (*requires SYNCHRONIZED*)
   let
     (*queue status*)
-    val _ = Multithreading.tracing 1 (fn () =>
+    val _ = Multithreading.tracing 6 (fn () =>
       let val {ready, pending, running} = Task_Queue.status (! queue) in
         "SCHEDULE: " ^
           string_of_int ready ^ " ready, " ^
@@ -338,8 +338,12 @@
         if SYNCHRONIZED "join_wait" (fn () =>
           is_finished x orelse (if worker then worker_wait () else wait (); false))
         then () else join_wait x;
-      val _ = List.app join_wait xs;
 
+      val _ = xs |> List.app (fn x =>
+        let val time = Multithreading.real_time join_wait x in
+          Multithreading.tracing_time true time
+            (fn () => "joined after " ^ Time.toString time)
+        end);
     in map get_result xs end) ();
 
 end;

--- a/src/Pure/Concurrent/simple_thread.ML	Sat Jul 25 00:39:05 2009 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML	Sat Jul 25 00:53:47 2009 +0200
@@ -31,7 +31,7 @@
         let
           val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ...");
           val time = Multithreading.real_time Mutex.lock lock;
-          val _ = Multithreading.tracing_time time
+          val _ = Multithreading.tracing_time true time
             (fn () => name ^ ": locked after " ^ Time.toString time);
         in false end;
     val result = Exn.capture (restore_attributes e) ();

--- a/src/Pure/ML-Systems/multithreading.ML	Sat Jul 25 00:39:05 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading.ML	Sat Jul 25 00:53:47 2009 +0200
@@ -15,7 +15,7 @@
   include BASIC_MULTITHREADING
   val trace: int ref
   val tracing: int -> (unit -> string) -> unit
-  val tracing_time: Time.time -> (unit -> string) -> unit
+  val tracing_time: bool -> Time.time -> (unit -> string) -> unit
   val real_time: ('a -> unit) -> 'a -> Time.time
   val available: bool
   val max_threads: int ref
@@ -37,7 +37,7 @@
 
 val trace = ref (0: int);
 fun tracing _ _ = ();
-fun tracing_time _ _ = ();
+fun tracing_time _ _ _ = ();
 fun real_time f x = (f x; Time.zeroTime);
 
 

--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Jul 25 00:39:05 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Jul 25 00:53:47 2009 +0200
@@ -36,9 +36,10 @@
   else (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
     handle _ (*sic*) => ();
 
-fun tracing_time time =
+fun tracing_time detailed time =
   tracing
-   (if Time.>= (time, Time.fromMilliseconds 1000) then 1
+   (if not detailed then 5
+    else if Time.>= (time, Time.fromMilliseconds 1000) then 1
     else if Time.>= (time, Time.fromMilliseconds 100) then 2
     else if Time.>= (time, Time.fromMilliseconds 10) then 3
     else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
@@ -231,7 +232,7 @@
             let
               val _ = tracing 5 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
               val time = real_time Mutex.lock critical_lock;
-              val _ = tracing_time time (fn () =>
+              val _ = tracing_time true time (fn () =>
                 "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time);
             in () end;
         val _ = critical_thread := SOME (Thread.self ());