src/Pure/ML-Systems/multithreading_polyml.ML
changeset 32186 8026b73cd357
parent 32185 57ecfab3bcfe
child 32230 9f6461b1c9cc
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Jul 25 00:39:05 2009 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Jul 25 00:53:47 2009 +0200
     1.3 @@ -36,9 +36,10 @@
     1.4    else (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
     1.5      handle _ (*sic*) => ();
     1.6  
     1.7 -fun tracing_time time =
     1.8 +fun tracing_time detailed time =
     1.9    tracing
    1.10 -   (if Time.>= (time, Time.fromMilliseconds 1000) then 1
    1.11 +   (if not detailed then 5
    1.12 +    else if Time.>= (time, Time.fromMilliseconds 1000) then 1
    1.13      else if Time.>= (time, Time.fromMilliseconds 100) then 2
    1.14      else if Time.>= (time, Time.fromMilliseconds 10) then 3
    1.15      else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
    1.16 @@ -231,7 +232,7 @@
    1.17              let
    1.18                val _ = tracing 5 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
    1.19                val time = real_time Mutex.lock critical_lock;
    1.20 -              val _ = tracing_time time (fn () =>
    1.21 +              val _ = tracing_time true time (fn () =>
    1.22                  "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time);
    1.23              in () end;
    1.24          val _ = critical_thread := SOME (Thread.self ());