end_timing: checked divisions with sane defaults;

--- a/src/Pure/ML-Systems/timing.ML	Mon Jun 22 22:49:44 2009 +0200
+++ b/src/Pure/ML-Systems/timing.ML	Mon Jun 22 22:51:08 2009 +0200
@@ -19,12 +19,16 @@
     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 * toReal gc / toReal cpu);
-    val factor = Real.fmt (StringCvt.FIX (SOME 2)) (toReal cpu / toReal elapsed);
+    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 => "";