# HG changeset patch
# User clasohm
# Date 824207775 -3600
# Node ID 4e617b8f97abb844197b37c651d407baf07b6352
# Parent  38a14548baadd073a83f606fe13a5f40420f6bd4
cond_timeit now uses totalCPUTimer instead of starting new ones every
time it is invoked; hopefully this will fix the strange SML109 bug

diff -r 38a14548baad -r 4e617b8f97ab src/Pure/NJ1xx.ML
--- a/src/Pure/NJ1xx.ML	Sat Feb 10 19:04:21 1996 +0100
+++ b/src/Pure/NJ1xx.ML	Tue Feb 13 11:36:15 1996 +0100
@@ -59,19 +59,21 @@
 
 (*** Timing functions ***)
 
+val CPUtimer = Timer.totalCPUTimer();
+
 (*A conditional timing function: applies f to () and, if the flag is true,
   prints its runtime. *)
 fun cond_timeit flag f =
   if flag then
-    let fun string_of_time t = Time.toString(t)
+    let open Time;
         open Timer;
-	open Time;
-        val start = startCPUTimer()
+        val {gc=gct1,sys=syst1,usr=usrt1} = checkCPUTimer(CPUtimer);
         val result = f();
-        val {gc=gct,sys=syst,usr=usrt} = checkCPUTimer(start)
-    in  print("Non GC " ^ string_of_time usrt ^
-               "   GC " ^ string_of_time gct ^
-               "  both+sys "^ string_of_time (syst+usrt+gct) ^ " secs\n");
+        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");
         result
     end
   else f();