CRITICAL: further trace levels for 1000ms and 100ms;

--- 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 ());