# HG changeset patch
# User paulson
# Date 844861091 -7200
# Node ID ec8857a115af92558464137ef22078ccd3db4e49
# Parent  2126029b881e3f0d679ef0f16eadddad40b5e8a4
cond_timeit now catches exception Time, which sml/nj
sometimes raised for no obvious reason

diff -r 2126029b881e -r ec8857a115af src/Pure/NJ1xx.ML
--- a/src/Pure/NJ1xx.ML	Wed Oct 09 13:37:00 1996 +0200
+++ b/src/Pure/NJ1xx.ML	Wed Oct 09 13:38:11 1996 +0200
@@ -65,15 +65,15 @@
   prints its runtime. *)
 fun cond_timeit flag f =
   if flag then
-    let open Time;
-        open Timer;
-        val {gc=gct1,sys=syst1,usr=usrt1} = checkCPUTimer(CPUtimer);
+    let open Time  (*...for Time.toString, Time.+ and Time.- *)
+	val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer);
         val result = f();
-        val {gc=gct2,sys=syst2,usr=usrt2} = checkCPUTimer(CPUtimer)
-    in  print("Non GC " ^ toString (usrt2-usrt1) ^
-              "   GC " ^ toString (gct2-gct1) ^
-              "  both+sys "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^
-              " secs\n");
+        val {gc=gct2,sys=syst2,usr=usrt2} = Timer.checkCPUTimer(CPUtimer)
+    in  print("User " ^ toString (usrt2-usrt1) ^
+              "  GC " ^ toString (gct2-gct1) ^
+              "  All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^
+              " secs\n")
+	  handle Time => ();
         result
     end
   else f();