synchronized: tuned tracing;
authorwenzelm
Sat, 18 Jul 2009 22:45:33 +0200
changeset 32051 82a9875b8707
parent 32050 ebb9274e34b7
child 32052 8c391a12df1d
synchronized: tuned tracing;
src/Pure/Concurrent/simple_thread.ML
--- a/src/Pure/Concurrent/simple_thread.ML	Sat Jul 18 00:34:22 2009 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML	Sat Jul 18 22:45:33 2009 +0200
@@ -25,13 +25,16 @@
 
 fun synchronized name lock e = Exn.release (uninterruptible (fn restore_attributes => fn () =>
   let
-    val _ =
-      if Mutex.trylock lock then ()
+    val immediate =
+      if Mutex.trylock lock then true
       else
        (Multithreading.tracing 3 (fn () => name ^ ": locking ...");
         Mutex.lock lock;
-        Multithreading.tracing 3 (fn () => name ^ ": ... locked"));
+        Multithreading.tracing 3 (fn () => name ^ ": locked");
+        false);
     val result = Exn.capture (restore_attributes e) ();
+    val _ =
+      if immediate then () else Multithreading.tracing 3 (fn () => name ^ ": unlocking ...");
     val _ = Mutex.unlock lock;
   in result end) ());