# HG changeset patch
# User wenzelm
# Date 1255554818 -7200
# Node ID 2218b970325aafad0fc8f1e3ea2ee90db982dab1
# Parent  a1b6e8d281ced2c87dae8fb64ff1df01193c95c0
show direct GC time (which is included in CPU time);

diff -r a1b6e8d281ce -r 2218b970325a src/Pure/ML-Systems/timing.ML
--- a/src/Pure/ML-Systems/timing.ML	Wed Oct 14 22:57:44 2009 +0200
+++ b/src/Pure/ML-Systems/timing.ML	Wed Oct 14 23:13:38 2009 +0200
@@ -19,18 +19,13 @@
     val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} =
       Timer.checkCPUTimes cpu_timer;
 
-    fun checked x y = Real.checkFloat y handle Overflow => x | Div => x;
-
     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_percent =
-      Real.fmt (StringCvt.FIX (SOME 1)) (100.0 * checked 0.0 (toReal gc / toReal cpu));
-    val factor =
-      Real.fmt (StringCvt.FIX (SOME 2)) (checked 1.0 (toReal cpu / toReal elapsed));
+
     val message =
       (toString elapsed ^ "s elapsed time, " ^ toString cpu ^ "s cpu time, " ^
-        gc_percent ^ "% GC time, factor " ^ factor) handle Time => "";
+        toString gc ^ "s GC time") handle Time.Time => "";
   in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end;