simplified/unified Multithreading.tracing_time;
tuned;

--- a/src/Pure/Concurrent/simple_thread.ML	Fri Jul 24 23:36:37 2009 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML	Sat Jul 25 00:13:39 2009 +0200
@@ -28,13 +28,17 @@
     val immediate =
       if Mutex.trylock lock then true
       else
-       (Multithreading.tracing 3 (fn () => name ^ ": locking ...");
-        Mutex.lock lock;
-        Multithreading.tracing 3 (fn () => name ^ ": locked");
-        false);
+        let
+          val timer = Timer.startRealTimer ();
+          val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ...");
+          val _ = Mutex.lock lock;
+          val time = Timer.checkRealTimer timer;
+          val _ = Multithreading.tracing_time time (fn () =>
+            name ^ ": locked after " ^ Time.toString time);
+        in false end;
     val result = Exn.capture (restore_attributes e) ();
     val _ =
-      if immediate then () else Multithreading.tracing 3 (fn () => name ^ ": unlocking ...");
+      if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ...");
     val _ = Mutex.unlock lock;
   in result end) ());
 

--- a/src/Pure/ML-Systems/multithreading.ML	Fri Jul 24 23:36:37 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading.ML	Sat Jul 25 00:13:39 2009 +0200
@@ -15,6 +15,7 @@
   include BASIC_MULTITHREADING
   val trace: int ref
   val tracing: int -> (unit -> string) -> unit
+  val tracing_time: Time.time -> (unit -> string) -> unit
   val available: bool
   val max_threads: int ref
   val max_threads_value: unit -> int
@@ -35,6 +36,7 @@
 
 val trace = ref (0: int);
 fun tracing _ _ = ();
+fun tracing_time _ _ = ();
 
 val available = false;
 val max_threads = ref (1: int);

--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Jul 24 23:36:37 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Jul 25 00:13:39 2009 +0200
@@ -36,6 +36,14 @@
   else (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
     handle _ (*sic*) => ();
 
+fun tracing_time time =
+  tracing
+   (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);
+
+
 val available = true;
 
 val max_threads = ref 0;
@@ -205,7 +213,7 @@
 fun NAMED_CRITICAL name e =
   if self_critical () then e ()
   else
-    uninterruptible (fn restore_attributes => fn () =>
+    Exn.release (uninterruptible (fn restore_attributes => fn () =>
       let
         val name' = ! critical_name;
         val _ =
@@ -213,14 +221,10 @@
           else
             let
               val timer = Timer.startRealTimer ();
-              val _ = tracing 4 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
+              val _ = tracing 5 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
               val _ = Mutex.lock critical_lock;
               val time = Timer.checkRealTimer timer;
-              val trace_time =
-                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 4;
-              val _ = tracing trace_time (fn () =>
+              val _ = tracing_time time (fn () =>
                 "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time);
             in () end;
         val _ = critical_thread := SOME (Thread.self ());
@@ -229,7 +233,7 @@
         val _ = critical_name := "";
         val _ = critical_thread := NONE;
         val _ = Mutex.unlock critical_lock;
-      in Exn.release result end) ();
+      in result end) ());
 
 fun CRITICAL e = NAMED_CRITICAL "" e;