# HG changeset patch
# User wenzelm
# Date 1245254571 -7200
# Node ID 8d1861721887543c99213262ba65cf5ac889b22e
# Parent  57715a08e4b634b8bedab880808fc8932b16a43a
end_timing: actually display GC percentage, not factor;

diff -r 57715a08e4b6 -r 8d1861721887 src/Pure/ML-Systems/timing.ML
--- a/src/Pure/ML-Systems/timing.ML	Wed Jun 17 17:24:34 2009 +0200
+++ b/src/Pure/ML-Systems/timing.ML	Wed Jun 17 18:02:51 2009 +0200
@@ -23,10 +23,10 @@
     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 gc_percent = Real.fmt (StringCvt.FIX (SOME 1)) (100.0 * 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 => "";
+        gc_percent ^ "% GC time, factor " ^ factor) handle Time => "";
   in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end;