src/Pure/ML-Systems/multithreading_polyml.ML

--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Jul 24 23:36:37 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Jul 25 00:13:39 2009 +0200
@@ -36,6 +36,14 @@
   else (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
     handle _ (*sic*) => ();
 
+fun tracing_time time =
+  tracing
+   (if Time.>= (time, Time.fromMilliseconds 1000) then 1
+    else if Time.>= (time, Time.fromMilliseconds 100) then 2
+    else if Time.>= (time, Time.fromMilliseconds 10) then 3
+    else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
+
+
 val available = true;
 
 val max_threads = ref 0;
@@ -205,7 +213,7 @@
 fun NAMED_CRITICAL name e =
   if self_critical () then e ()
   else
-    uninterruptible (fn restore_attributes => fn () =>
+    Exn.release (uninterruptible (fn restore_attributes => fn () =>
       let
         val name' = ! critical_name;
         val _ =
@@ -213,14 +221,10 @@
           else
             let
               val timer = Timer.startRealTimer ();
-              val _ = tracing 4 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
+              val _ = tracing 5 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
               val _ = Mutex.lock critical_lock;
               val time = Timer.checkRealTimer timer;
-              val trace_time =
-                if Time.>= (time, Time.fromMilliseconds 1000) then 1
-                else if Time.>= (time, Time.fromMilliseconds 100) then 2
-                else if Time.>= (time, Time.fromMilliseconds 10) then 3 else 4;
-              val _ = tracing trace_time (fn () =>
+              val _ = tracing_time time (fn () =>
                 "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time);
             in () end;
         val _ = critical_thread := SOME (Thread.self ());
@@ -229,7 +233,7 @@
         val _ = critical_name := "";
         val _ = critical_thread := NONE;
         val _ = Mutex.unlock critical_lock;
-      in Exn.release result end) ();
+      in result end) ());
 
 fun CRITICAL e = NAMED_CRITICAL "" e;