more detailed start_timing/end_timing (in timing.ML);
removed obsolete check_timer;

--- a/src/Pure/IsaMakefile	Wed Jun 17 17:06:07 2009 +0200
+++ b/src/Pure/IsaMakefile	Wed Jun 17 17:06:07 2009 +0200
@@ -29,7 +29,8 @@
   ML-Systems/polyml.ML ML-Systems/polyml_common.ML			\
   ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML	\
   ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML			\
-  ML-Systems/time_limit.ML ML-Systems/universal.ML
+  ML-Systems/timing.ML ML-Systems/time_limit.ML				\
+  ML-Systems/universal.ML
 
 RAW: $(OUT)/RAW
 

--- a/src/Pure/ML-Systems/mosml.ML	Wed Jun 17 17:06:07 2009 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Wed Jun 17 17:06:07 2009 +0200
@@ -154,10 +154,6 @@
     val message = "User " ^ toString user ^ "  All "^ toString all ^ " secs" handle Time => "";
   in {message = message, user = user, all = all} end;
 
-fun check_timer timer =
-  let val {sys, usr, gc} = Timer.checkCPUTimer timer
-  in (sys, usr, gc) end;
-
 
 (* SML basis library fixes *)
 

--- a/src/Pure/ML-Systems/polyml_common.ML	Wed Jun 17 17:06:07 2009 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Wed Jun 17 17:06:07 2009 +0200
@@ -8,6 +8,7 @@
 use "ML-Systems/exn.ML";
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
+use "ML-Systems/timing.ML";
 use "ML-Systems/system_shell.ML";
 use "ML-Systems/ml_pretty.ML";
 use "ML-Systems/use_context.ML";
@@ -41,30 +42,6 @@
 val implode = SML90.implode;
 
 
-(* compiler-independent timing functions *)
-
-fun start_timing () =
-  let
-    val timer = Timer.startCPUTimer ();
-    val time = Timer.checkCPUTimer timer;
-  in (timer, time) end;
-
-fun end_timing (timer, {sys, usr}) =
-  let
-    open Time;  (*...for Time.toString, Time.+ and Time.- *)
-    val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
-    val user = usr2 - usr;
-    val all = user + sys2 - sys;
-    val message = "User " ^ toString user ^ "  All "^ toString all ^ " secs" handle Time => "";
-  in {message = message, user = user, all = all} end;
-
-fun check_timer timer =
-  let
-    val {sys, usr} = Timer.checkCPUTimer timer;
-    val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
-  in (sys, usr, gc) end;
-
-
 (* prompts *)
 
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);

--- a/src/Pure/ML-Systems/smlnj.ML	Wed Jun 17 17:06:07 2009 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Jun 17 17:06:07 2009 +0200
@@ -12,6 +12,7 @@
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/multithreading.ML";
+use "ML-Systems/timing.ML";
 use "ML-Systems/system_shell.ML";
 use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/ml_pretty.ML";
@@ -59,30 +60,6 @@
 end;
 
 
-(* compiler-independent timing functions *)
-
-fun start_timing () =
-  let
-    val timer = Timer.startCPUTimer ();
-    val time = Timer.checkCPUTimer timer;
-  in (timer, time) end;
-
-fun end_timing (timer, {sys, usr}) =
-  let
-    open Time;  (*...for Time.toString, Time.+ and Time.- *)
-    val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
-    val user = usr2 - usr;
-    val all = user + sys2 - sys;
-    val message = "User " ^ toString user ^ "  All "^ toString all ^ " secs" handle Time => "";
-  in {message = message, user = user, all = all} end;
-
-fun check_timer timer =
-  let
-    val {sys, usr} = Timer.checkCPUTimer timer;
-    val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
-  in (sys, usr, gc) end;
-
-
 (*prompts*)
 fun ml_prompts p1 p2 =
   (Control.primaryPrompt := p1; Control.secondaryPrompt := p2);

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/timing.ML	Wed Jun 17 17:06:07 2009 +0200
@@ -0,0 +1,32 @@
+(*  Title:      Pure/ML-Systems/timing.ML
+    Author:     Makarius
+
+Compiler-independent timing functions.
+*)
+
+fun start_timing () =
+  let
+    val real_timer = Timer.startRealTimer ();
+    val real_time = Timer.checkRealTimer real_timer;
+    val cpu_timer = Timer.startCPUTimer ();
+    val cpu_times = Timer.checkCPUTimes cpu_timer;
+  in (real_timer, real_time, cpu_timer, cpu_times) end;
+
+fun end_timing (real_timer, real_time, cpu_timer, cpu_times) =
+  let
+    val real_time2 = Timer.checkRealTimer real_timer;
+    val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;
+    val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} =
+      Timer.checkCPUTimes cpu_timer;
+
+    open Time;
+    val elapsed = real_time2 - real_time;
+    val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
+    val cpu = usr2 - usr + sys2 - sys + gc;
+    val gc_ratio = Real.fmt (StringCvt.FIX (SOME 2)) (toReal gc / toReal cpu);
+    val factor = Real.fmt (StringCvt.FIX (SOME 2)) (toReal cpu / toReal elapsed);
+    val message =
+      (toString elapsed ^ "s elapsed time, " ^ toString cpu ^ "s cpu time, " ^
+        gc_ratio ^ "% GC time, factor " ^ factor) handle Time => "";
+  in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end;
+