1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jul 25 22:20:52 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jul 25 22:20:53 2007 +0200
     1.3 @@ -34,23 +34,25 @@
     1.4      NONE => false
     1.5    | SOME id => Thread.equal (id, Thread.self ()));
     1.6  
     1.7 -fun CRITICAL' name e =
     1.8 +fun NAMED_CRITICAL name e =
     1.9    if self_critical () then e ()
    1.10    else
    1.11      let
    1.12        val _ =
    1.13          if Mutex.trylock critical_lock then ()
    1.14          else
    1.15 -         (tracing (fn () => "CRITICAL " ^ name ^ ": waiting for lock");
    1.16 +         (tracing (fn () =>
    1.17 +            "CRITICAL" ^ (if name = "" then "" else " " ^ name) ^ ": waiting for lock");
    1.18            Mutex.lock critical_lock;
    1.19 -          tracing (fn () => "CRITICAL " ^ name ^ ": obtained lock"));
    1.20 +          tracing (fn () =>
    1.21 +            "CRITICAL" ^ (if name = "" then "" else " " ^ name) ^ ": obtained lock"));
    1.22        val _ = critical_thread := SOME (Thread.self ());
    1.23        val result = Exn.capture e ();
    1.24        val _ = critical_thread := NONE;
    1.25        val _ = Mutex.unlock critical_lock;
    1.26      in Exn.release result end;
    1.27  
    1.28 -fun CRITICAL e = CRITICAL' "" e;
    1.29 +fun CRITICAL e = NAMED_CRITICAL "" e;
    1.30  
    1.31  end;
    1.32  
    1.33 @@ -117,5 +119,5 @@
    1.34  
    1.35  end;
    1.36  
    1.37 -val CRITICAL' = Multithreading.CRITICAL';
    1.38 +val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
    1.39  val CRITICAL = Multithreading.CRITICAL;