somewhat more uniform timing in ML vs. Scala;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/timing.ML	Sat Nov 06 17:55:32 2010 +0100
@@ -0,0 +1,36 @@
+(*  Title:      Pure/General/timing.ML
+    Author:     Makarius
+
+Basic support for time measurement.
+*)
+
+val seconds = Time.fromReal;
+
+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;
+
+type timing = {message: string, elapsed: Time.time, cpu: Time.time, gc: Time.time};
+
+fun end_timing (real_timer, real_time, cpu_timer, cpu_times) : timing =
+  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 message =
+     (toString elapsed ^ "s elapsed time, " ^
+      toString cpu ^ "s cpu time, " ^
+      toString gc ^ "s GC time") handle Time.Time => "";
+  in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end;
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/timing.scala	Sat Nov 06 17:55:32 2010 +0100
@@ -0,0 +1,20 @@
+/*  Title:      Pure/General/timing.scala
+    Author:     Makarius
+
+Basic support for time measurement.
+*/
+
+package isabelle
+
+
+sealed case class Timing(val elapsed: Double, cpu: Double, gc: Double)
+{
+  private def print_time(seconds: Double): String =
+    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
+
+  def message: String =
+    print_time(elapsed) + "s elapsed time, " +
+    print_time(cpu) + "s cpu time, " +
+    print_time(gc) + "s GC time"
+}
+

--- a/src/Pure/IsaMakefile	Sat Nov 06 16:53:07 2010 +0100
+++ b/src/Pure/IsaMakefile	Sat Nov 06 17:55:32 2010 +0100
@@ -21,6 +21,7 @@
 
 BOOTSTRAP_FILES = 					\
   General/exn.ML					\
+  General/timing.ML					\
   ML-Systems/bash.ML 					\
   ML-Systems/compiler_polyml-5.2.ML			\
   ML-Systems/compiler_polyml-5.3.ML			\
@@ -41,7 +42,6 @@
   ML-Systems/smlnj.ML					\
   ML-Systems/thread_dummy.ML				\
   ML-Systems/time_limit.ML				\
-  ML-Systems/timing.ML					\
   ML-Systems/universal.ML				\
   ML-Systems/unsynchronized.ML				\
   ML-Systems/use_context.ML

--- a/src/Pure/ML-Systems/polyml_common.ML	Sat Nov 06 16:53:07 2010 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Sat Nov 06 17:55:32 2010 +0100
@@ -13,7 +13,7 @@
 
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
-use "ML-Systems/timing.ML";
+use "General/timing.ML";
 use "ML-Systems/bash.ML";
 use "ML-Systems/ml_pretty.ML";
 use "ML-Systems/use_context.ML";

--- a/src/Pure/ML-Systems/smlnj.ML	Sat Nov 06 16:53:07 2010 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Sat Nov 06 17:55:32 2010 +0100
@@ -13,7 +13,7 @@
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/multithreading.ML";
-use "ML-Systems/timing.ML";
+use "General/timing.ML";
 use "ML-Systems/bash.ML";
 use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/ml_pretty.ML";

--- a/src/Pure/ML-Systems/timing.ML	Sat Nov 06 16:53:07 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(*  Title:      Pure/ML-Systems/timing.ML
-    Author:     Makarius
-
-Basic support for time measurement.
-*)
-
-val seconds = Time.fromReal;
-
-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;
-
-type timing = {message: string, elapsed: Time.time, cpu: Time.time, gc: Time.time};
-
-fun end_timing (real_timer, real_time, cpu_timer, cpu_times) : timing =
-  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 message =
-      (toString elapsed ^ "s elapsed time, " ^ toString cpu ^ "s cpu time, " ^
-        toString gc ^ "s GC time") handle Time.Time => "";
-  in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end;
-

--- a/src/Pure/build-jars	Sat Nov 06 16:53:07 2010 +0100
+++ b/src/Pure/build-jars	Sat Nov 06 17:55:32 2010 +0100
@@ -26,6 +26,7 @@
   Concurrent/simple_thread.scala
   Concurrent/volatile.scala
   General/exn.scala
+  General/timing.scala
   General/linear_set.scala
   General/markup.scala
   General/position.scala