src/Pure/ML-Systems/multithreading_polyml.ML
changeset 32184 cfa0ef0c0c5f
parent 32107 47d0da617fcc
child 32185 57ecfab3bcfe
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Jul 24 23:36:37 2009 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Jul 25 00:13:39 2009 +0200
     1.3 @@ -36,6 +36,14 @@
     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 +  tracing
     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
    1.12 +    else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
    1.13 +
    1.14 +
    1.15  val available = true;
    1.16  
    1.17  val max_threads = ref 0;
    1.18 @@ -205,7 +213,7 @@
    1.19  fun NAMED_CRITICAL name e =
    1.20    if self_critical () then e ()
    1.21    else
    1.22 -    uninterruptible (fn restore_attributes => fn () =>
    1.23 +    Exn.release (uninterruptible (fn restore_attributes => fn () =>
    1.24        let
    1.25          val name' = ! critical_name;
    1.26          val _ =
    1.27 @@ -213,14 +221,10 @@
    1.28            else
    1.29              let
    1.30                val timer = Timer.startRealTimer ();
    1.31 -              val _ = tracing 4 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
    1.32 +              val _ = tracing 5 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
    1.33                val _ = Mutex.lock critical_lock;
    1.34                val time = Timer.checkRealTimer timer;
    1.35 -              val trace_time =
    1.36 -                if Time.>= (time, Time.fromMilliseconds 1000) then 1
    1.37 -                else if Time.>= (time, Time.fromMilliseconds 100) then 2
    1.38 -                else if Time.>= (time, Time.fromMilliseconds 10) then 3 else 4;
    1.39 -              val _ = tracing trace_time (fn () =>
    1.40 +              val _ = tracing_time time (fn () =>
    1.41                  "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time);
    1.42              in () end;
    1.43          val _ = critical_thread := SOME (Thread.self ());
    1.44 @@ -229,7 +233,7 @@
    1.45          val _ = critical_name := "";
    1.46          val _ = critical_thread := NONE;
    1.47          val _ = Mutex.unlock critical_lock;
    1.48 -      in Exn.release result end) ();
    1.49 +      in result end) ());
    1.50  
    1.51  fun CRITICAL e = NAMED_CRITICAL "" e;
    1.52