# HG changeset patch
# User wenzelm
# Date 1481708425 -3600
# Node ID 20e361014f55c4dc0aa4155e168a9eba4b8e8875
# Parent  e154ec4e3eacb59c85fd64932b0c89a66f0c8184
tuned;

diff -r e154ec4e3eac -r 20e361014f55 src/Pure/Concurrent/multithreading.ML
--- a/src/Pure/Concurrent/multithreading.ML	Wed Dec 14 10:29:47 2016 +0100
+++ b/src/Pure/Concurrent/multithreading.ML	Wed Dec 14 10:40:25 2016 +0100
@@ -79,20 +79,27 @@
 
 fun synchronized name lock e =
   Exn.release (Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
-    let
-      val immediate =
-        if Mutex.trylock lock then true
-        else
-          let
-            val _ = tracing 5 (fn () => name ^ ": locking ...");
-            val timer = Timer.startRealTimer ();
-            val _ = Mutex.lock lock;
-            val time = Timer.checkRealTimer timer;
-            val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
-          in false end;
-      val result = Exn.capture (restore_attributes e) ();
-      val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
-      val _ = Mutex.unlock lock;
-    in result end) ());
+    if ! trace > 0 then
+      let
+        val immediate =
+          if Mutex.trylock lock then true
+          else
+            let
+              val _ = tracing 5 (fn () => name ^ ": locking ...");
+              val timer = Timer.startRealTimer ();
+              val _ = Mutex.lock lock;
+              val time = Timer.checkRealTimer timer;
+              val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
+            in false end;
+        val result = Exn.capture (restore_attributes e) ();
+        val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
+        val _ = Mutex.unlock lock;
+      in result end
+    else
+      let
+        val _ = Mutex.lock lock;
+        val result = Exn.capture (restore_attributes e) ();
+        val _ = Mutex.unlock lock;
+      in result end) ());
 
 end;