src/Pure/ML-Systems/multithreading_polyml.ML

 
 fun tracing level msg =
   if level > ! trace then ()
   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;
 

   | SOME t => Thread.equal (t, Thread.self ()));
 
 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 _ =
           if Mutex.trylock critical_lock then ()
           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 ());
         val _ = critical_name := name;
         val result = Exn.capture (restore_attributes e) ();
         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;
 
 end;