tuned;
authorwenzelm
Wed Dec 14 10:40:25 2016 +0100 (2016-12-14)
changeset 6456320e361014f55
parent 64562 e154ec4e3eac
child 64564 fc66a76d6b95
tuned;
src/Pure/Concurrent/multithreading.ML
     1.1 --- a/src/Pure/Concurrent/multithreading.ML	Wed Dec 14 10:29:47 2016 +0100
     1.2 +++ b/src/Pure/Concurrent/multithreading.ML	Wed Dec 14 10:40:25 2016 +0100
     1.3 @@ -79,20 +79,27 @@
     1.4  
     1.5  fun synchronized name lock e =
     1.6    Exn.release (Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     1.7 -    let
     1.8 -      val immediate =
     1.9 -        if Mutex.trylock lock then true
    1.10 -        else
    1.11 -          let
    1.12 -            val _ = tracing 5 (fn () => name ^ ": locking ...");
    1.13 -            val timer = Timer.startRealTimer ();
    1.14 -            val _ = Mutex.lock lock;
    1.15 -            val time = Timer.checkRealTimer timer;
    1.16 -            val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
    1.17 -          in false end;
    1.18 -      val result = Exn.capture (restore_attributes e) ();
    1.19 -      val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
    1.20 -      val _ = Mutex.unlock lock;
    1.21 -    in result end) ());
    1.22 +    if ! trace > 0 then
    1.23 +      let
    1.24 +        val immediate =
    1.25 +          if Mutex.trylock lock then true
    1.26 +          else
    1.27 +            let
    1.28 +              val _ = tracing 5 (fn () => name ^ ": locking ...");
    1.29 +              val timer = Timer.startRealTimer ();
    1.30 +              val _ = Mutex.lock lock;
    1.31 +              val time = Timer.checkRealTimer timer;
    1.32 +              val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
    1.33 +            in false end;
    1.34 +        val result = Exn.capture (restore_attributes e) ();
    1.35 +        val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
    1.36 +        val _ = Mutex.unlock lock;
    1.37 +      in result end
    1.38 +    else
    1.39 +      let
    1.40 +        val _ = Mutex.lock lock;
    1.41 +        val result = Exn.capture (restore_attributes e) ();
    1.42 +        val _ = Mutex.unlock lock;
    1.43 +      in result end) ());
    1.44  
    1.45  end;