src/Pure/ML-Systems/multithreading_polyml.ML
changeset 26493 de4764e95166
parent 26390 99d4cbb1f941
child 26504 6e87c0a60104
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Mar 29 19:14:14 2008 +0100
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Mar 29 19:14:15 2008 +0100
     1.3 @@ -218,7 +218,11 @@
     1.4                val _ = tracing 4 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
     1.5                val _ = Mutex.lock critical_lock;
     1.6                val time = Timer.checkRealTimer timer;
     1.7 -              val _ = tracing (if Time.> (time, Time.fromMilliseconds 10) then 3 else 4) (fn () =>
     1.8 +              val trace_time =
     1.9 +                if Time.>= (time, Time.fromMilliseconds 1000) then 1
    1.10 +                else if Time.>= (time, Time.fromMilliseconds 100) then 2
    1.11 +                else if Time.>= (time, Time.fromMilliseconds 10) then 3 else 4;
    1.12 +              val _ = tracing trace_time (fn () =>
    1.13                  "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time);
    1.14              in () end;
    1.15          val _ = critical_thread := SOME (Thread.self ());