added Multithreading.real_time;

--- a/src/Pure/Concurrent/simple_thread.ML	Sat Jul 25 00:13:39 2009 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML	Sat Jul 25 00:39:05 2009 +0200
@@ -29,12 +29,10 @@
       if Mutex.trylock lock then true
       else
         let
-          val timer = Timer.startRealTimer ();
           val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ...");
-          val _ = Mutex.lock lock;
-          val time = Timer.checkRealTimer timer;
-          val _ = Multithreading.tracing_time time (fn () =>
-            name ^ ": locked after " ^ Time.toString time);
+          val time = Multithreading.real_time Mutex.lock lock;
+          val _ = Multithreading.tracing_time time
+            (fn () => name ^ ": locked after " ^ Time.toString time);
         in false end;
     val result = Exn.capture (restore_attributes e) ();
     val _ =

--- a/src/Pure/ML-Systems/multithreading.ML	Sat Jul 25 00:13:39 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading.ML	Sat Jul 25 00:39:05 2009 +0200
@@ -16,6 +16,7 @@
   val trace: int ref
   val tracing: int -> (unit -> string) -> unit
   val tracing_time: Time.time -> (unit -> string) -> unit
+  val real_time: ('a -> unit) -> 'a -> Time.time
   val available: bool
   val max_threads: int ref
   val max_threads_value: unit -> int
@@ -32,11 +33,15 @@
 structure Multithreading: MULTITHREADING =
 struct
 
-(* options *)
+(* tracing *)
 
 val trace = ref (0: int);
 fun tracing _ _ = ();
 fun tracing_time _ _ = ();
+fun real_time f x = (f x; Time.zeroTime);
+
+
+(* options *)
 
 val available = false;
 val max_threads = ref (1: int);

--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Jul 25 00:13:39 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Jul 25 00:39:05 2009 +0200
@@ -27,7 +27,7 @@
 structure Multithreading: MULTITHREADING =
 struct
 
-(* options *)
+(* tracing *)
 
 val trace = ref 0;
 
@@ -43,6 +43,15 @@
     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;
 
@@ -220,10 +229,8 @@
           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;