# HG changeset patch
# User wenzelm
# Date 1247949933 -7200
# Node ID 82a9875b8707485ca17f1b3ecc3dd7435198cada
# Parent  ebb9274e34b74e07051d94e991db1fd38a7d2a47
synchronized: tuned tracing;

diff -r ebb9274e34b7 -r 82a9875b8707 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) ());