# HG changeset patch
# User wenzelm
# Date 1206814455 -3600
# Node ID de4764e951664f7fd8d096f2b77d4caf35b10307
# Parent  6e87cc839632f2f666e68047e15a30697382c576
CRITICAL: further trace levels for 1000ms and 100ms;

diff -r 6e87cc839632 -r de4764e95166 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Mar 29 19:14:14 2008 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Mar 29 19:14:15 2008 +0100
@@ -218,7 +218,11 @@
               val _ = tracing 4 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
               val _ = Mutex.lock critical_lock;
               val time = Timer.checkRealTimer timer;
-              val _ = tracing (if Time.> (time, Time.fromMilliseconds 10) then 3 else 4) (fn () =>
+              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 () =>
                 "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time);
             in () end;
         val _ = critical_thread := SOME (Thread.self ());