src/Pure/ML-Systems/multithreading_polyml.ML

 end;
 
 structure Multithreading: MULTITHREADING =
 struct
 
-(* options *)
+(* tracing *)
 
 val trace = ref 0;
 
 fun tracing level msg =
   if level > ! trace then ()

    (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 if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
 
+fun real_time f x =
+  let
+    val timer = Timer.startRealTimer ();
+    val () = f x;
+    val time = Timer.checkRealTimer timer;
+  in time end;
+
+
+(* options *)
 
 val available = true;
 
 val max_threads = ref 0;
 

         val name' = ! critical_name;
         val _ =
           if Mutex.trylock critical_lock then ()
           else
             let
-              val timer = Timer.startRealTimer ();
               val _ = tracing 5 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
-              val _ = Mutex.lock critical_lock;
-              val time = Timer.checkRealTimer timer;
+              val time = real_time Mutex.lock critical_lock;
               val _ = tracing_time time (fn () =>
                 "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time);
             in () end;
         val _ = critical_thread := SOME (Thread.self ());
         val _ = critical_name := name;