# HG changeset patch
# User wenzelm
# Date 1185394853 -7200
# Node ID d4417ba26706e239a3444b32fb6866c5dfd18e89
# Parent  72a9b436af5677e6644dbc0b75e11312d75773a6
renamed CRITICAL' to NAMED_CRITICAL;
tuned messages;

diff -r 72a9b436af56 -r d4417ba26706 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jul 25 22:20:52 2007 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jul 25 22:20:53 2007 +0200
@@ -34,23 +34,25 @@
     NONE => false
   | SOME id => Thread.equal (id, Thread.self ()));
 
-fun CRITICAL' name e =
+fun NAMED_CRITICAL name e =
   if self_critical () then e ()
   else
     let
       val _ =
         if Mutex.trylock critical_lock then ()
         else
-         (tracing (fn () => "CRITICAL " ^ name ^ ": waiting for lock");
+         (tracing (fn () =>
+            "CRITICAL" ^ (if name = "" then "" else " " ^ name) ^ ": waiting for lock");
           Mutex.lock critical_lock;
-          tracing (fn () => "CRITICAL " ^ name ^ ": obtained lock"));
+          tracing (fn () =>
+            "CRITICAL" ^ (if name = "" then "" else " " ^ name) ^ ": obtained lock"));
       val _ = critical_thread := SOME (Thread.self ());
       val result = Exn.capture e ();
       val _ = critical_thread := NONE;
       val _ = Mutex.unlock critical_lock;
     in Exn.release result end;
 
-fun CRITICAL e = CRITICAL' "" e;
+fun CRITICAL e = NAMED_CRITICAL "" e;
 
 end;
 
@@ -117,5 +119,5 @@
 
 end;
 
-val CRITICAL' = Multithreading.CRITICAL';
+val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
 val CRITICAL = Multithreading.CRITICAL;