src/Pure/Concurrent/simple_thread.ML
changeset 32051 82a9875b8707
parent 29564 f8b933a62151
child 32184 cfa0ef0c0c5f
     1.1 --- a/src/Pure/Concurrent/simple_thread.ML	Sat Jul 18 00:34:22 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/simple_thread.ML	Sat Jul 18 22:45:33 2009 +0200
     1.3 @@ -25,13 +25,16 @@
     1.4  
     1.5  fun synchronized name lock e = Exn.release (uninterruptible (fn restore_attributes => fn () =>
     1.6    let
     1.7 -    val _ =
     1.8 -      if Mutex.trylock lock then ()
     1.9 +    val immediate =
    1.10 +      if Mutex.trylock lock then true
    1.11        else
    1.12         (Multithreading.tracing 3 (fn () => name ^ ": locking ...");
    1.13          Mutex.lock lock;
    1.14 -        Multithreading.tracing 3 (fn () => name ^ ": ... locked"));
    1.15 +        Multithreading.tracing 3 (fn () => name ^ ": locked");
    1.16 +        false);
    1.17      val result = Exn.capture (restore_attributes e) ();
    1.18 +    val _ =
    1.19 +      if immediate then () else Multithreading.tracing 3 (fn () => name ^ ": unlocking ...");
    1.20      val _ = Mutex.unlock lock;
    1.21    in result end) ());
    1.22