end_timing: generalized result -- message plus with explicit time values;

--- a/src/Provers/blast.ML	Sun Mar 01 14:45:23 2009 +0100
+++ b/src/Provers/blast.ML	Sun Mar 01 16:21:33 2009 +0100
@@ -913,7 +913,7 @@
 
 fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) =
   if b then
-    writeln (end_timing start ^ " for search.  Closed: "
+    writeln (#message (end_timing start) ^ " for search.  Closed: "
              ^ Int.toString (!nclosed) ^
              " tried: " ^ Int.toString (!ntried) ^
              " tactics: " ^ Int.toString (length tacs))
@@ -1264,7 +1264,7 @@
                        else ();
                        backtrack choices)
             | cell => (if (!trace orelse !stats)
-                       then writeln (end_timing start ^ " for reconstruction")
+                       then writeln (#message (end_timing start) ^ " for reconstruction")
                        else ();
                        Seq.make(fn()=> cell))
           end

--- a/src/Pure/General/output.ML	Sun Mar 01 14:45:23 2009 +0100
+++ b/src/Pure/General/output.ML	Sun Mar 01 16:21:33 2009 +0100
@@ -135,7 +135,7 @@
     let
       val start = start_timing ();
       val result = Exn.capture e ();
-      val end_msg = end_timing start;
+      val end_msg = #message (end_timing start);
       val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
     in Exn.release result end
   else e ();

--- a/src/Pure/ML-Systems/mosml.ML	Sun Mar 01 14:45:23 2009 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Sun Mar 01 16:21:33 2009 +0100
@@ -141,19 +141,19 @@
 load "Timer";
 
 fun start_timing () =
-  let val CPUtimer = Timer.startCPUTimer();
-      val time = Timer.checkCPUTimer(CPUtimer)
-  in  (CPUtimer,time)  end;
+  let
+    val timer = Timer.startCPUTimer ();
+    val time = Timer.checkCPUTimer timer;
+  in (timer, time) end;
 
-fun end_timing (CPUtimer, {gc,sys,usr}) =
-  let open Time  (*...for Time.toString, Time.+ and Time.- *)
-      val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
-  in  "User " ^ toString (usr2-usr) ^
-      "  GC " ^ toString (gc2-gc) ^
-      "  All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^
-      " secs"
-      handle Time => ""
-  end;
+fun end_timing (timer, {gc, sys, usr}) =
+  let
+    open Time;  (*...for Time.toString, Time.+ and Time.- *)
+    val {gc = gc2, sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
+    val user = usr2 - usr + gc2 - gc;
+    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, gc} = Timer.checkCPUTimer timer

--- a/src/Pure/ML-Systems/polyml_common.ML	Sun Mar 01 14:45:23 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Sun Mar 01 16:21:33 2009 +0100
@@ -47,18 +47,19 @@
 (* compiler-independent timing functions *)
 
 fun start_timing () =
-  let val CPUtimer = Timer.startCPUTimer();
-      val time = Timer.checkCPUTimer(CPUtimer)
-  in  (CPUtimer,time)  end;
+  let
+    val timer = Timer.startCPUTimer ();
+    val time = Timer.checkCPUTimer timer;
+  in (timer, time) end;
 
-fun end_timing (CPUtimer, {sys,usr}) =
-  let open Time  (*...for Time.toString, Time.+ and Time.- *)
-      val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
-  in  "User " ^ toString (usr2-usr) ^
-      "  All "^ toString (sys2-sys + usr2-usr) ^
-      " secs"
-      handle 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

--- a/src/Pure/ML-Systems/smlnj.ML	Sun Mar 01 14:45:23 2009 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Sun Mar 01 16:21:33 2009 +0100
@@ -59,18 +59,19 @@
 (* compiler-independent timing functions *)
 
 fun start_timing () =
-  let val CPUtimer = Timer.startCPUTimer();
-      val time = Timer.checkCPUTimer(CPUtimer)
-  in  (CPUtimer,time)  end;
+  let
+    val timer = Timer.startCPUTimer ();
+    val time = Timer.checkCPUTimer timer;
+  in (timer, time) end;
 
-fun end_timing (CPUtimer, {sys,usr}) =
-  let open Time  (*...for Time.toString, Time.+ and Time.- *)
-      val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
-  in  "User " ^ toString (usr2-usr) ^
-      "  All "^ toString (sys2-sys + usr2-usr) ^
-      " secs"
-      handle 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

--- a/src/Tools/Compute_Oracle/report.ML	Sun Mar 01 14:45:23 2009 +0100
+++ b/src/Tools/Compute_Oracle/report.ML	Sun Mar 01 16:21:33 2009 +0100
@@ -13,7 +13,7 @@
     let
 	val t1 = start_timing ()
 	val x = f ()
-	val t2 = end_timing t1
+	val t2 = #message (end_timing t1)
 	val _ = writeln ((report_space ()) ^ "--> "^t2)
     in
 	x