src/Pure/ML-Systems/multithreading_polyml.ML
changeset 32185 57ecfab3bcfe
parent 32184 cfa0ef0c0c5f
child 32186 8026b73cd357
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Jul 25 00:13:39 2009 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Jul 25 00:39:05 2009 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  structure Multithreading: MULTITHREADING =
     1.5  struct
     1.6  
     1.7 -(* options *)
     1.8 +(* tracing *)
     1.9  
    1.10  val trace = ref 0;
    1.11  
    1.12 @@ -43,6 +43,15 @@
    1.13      else if Time.>= (time, Time.fromMilliseconds 10) then 3
    1.14      else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
    1.15  
    1.16 +fun real_time f x =
    1.17 +  let
    1.18 +    val timer = Timer.startRealTimer ();
    1.19 +    val () = f x;
    1.20 +    val time = Timer.checkRealTimer timer;
    1.21 +  in time end;
    1.22 +
    1.23 +
    1.24 +(* options *)
    1.25  
    1.26  val available = true;
    1.27  
    1.28 @@ -220,10 +229,8 @@
    1.29            if Mutex.trylock critical_lock then ()
    1.30            else
    1.31              let
    1.32 -              val timer = Timer.startRealTimer ();
    1.33                val _ = tracing 5 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
    1.34 -              val _ = Mutex.lock critical_lock;
    1.35 -              val time = Timer.checkRealTimer timer;
    1.36 +              val time = real_time Mutex.lock critical_lock;
    1.37                val _ = tracing_time time (fn () =>
    1.38                  "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time);
    1.39              in () end;