# HG changeset patch
# User paulson
# Date 880711154 -3600
# Node ID 7211ea5f29e2c1989ed658169cdf4bba2dc3bdd0
# Parent  e72cba5af6c57002773c2a0dd01611c78c44a5fc
New timing functions startTiming and endTiming

diff -r e72cba5af6c5 -r 7211ea5f29e2 src/Pure/ML-Systems/MLWorks.ML
--- a/src/Pure/ML-Systems/MLWorks.ML	Fri Nov 28 10:54:13 1997 +0100
+++ b/src/Pure/ML-Systems/MLWorks.ML	Fri Nov 28 10:59:14 1997 +0100
@@ -44,25 +44,24 @@
 val implode = String.concat;
 
 
-(*** Timing functions ***)
+(** Compiler-independent timing functions **)
+
+(*Note start point for timing*)
+fun startTiming() = 
+  let val CPUtimer = Timer.startCPUTimer();
+      val time = Timer.checkCPUTimer(CPUtimer)
+  in  (CPUtimer,time)  end;
 
-(*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 open Time  (*...for Time.toString, Time.+ and Time.- *)
-	val CPUtimer = Timer.startCPUTimer();
-        val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer);
-        val result = f();
-        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();
+(*Finish timing and return string*)
+fun endTiming (CPUtimer, {gc,sys,usr}) =
+  let open Time  (*...for Time.toString, Time.+ and Time.- *)
+      val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
+  in  "User " ^ toString (usr2-usr) ^
+      "  GC " ^ toString (gc2-gc) ^
+      "  All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^
+      " secs"
+      handle Time => ""
+  end;
 
 
 (*** File handling ***)
@@ -103,16 +102,10 @@
 
 (* getenv *)
 
-local
-  fun drop_last [] = []
-    | drop_last [x] = []
-    | drop_last (x :: xs) = x :: drop_last xs;
-
-  val drop_last_char = implode o drop_last o explode;
-in
-  fun getenv var = drop_last_char
-    (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
-end;
+fun getenv var =
+  (case OS.Process.getEnv var of
+    NONE => ""
+  | SOME txt => txt);
 
 
 (*Non-printing and 8-bit chars are forbidden in string constants*)
diff -r e72cba5af6c5 -r 7211ea5f29e2 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Fri Nov 28 10:54:13 1997 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Fri Nov 28 10:59:14 1997 +0100
@@ -15,22 +15,16 @@
 
 (** ML system related **)
 
-(* timing *)
+(** Compiler-independent timing functions **)
 
-(*a conditional timing function: applies f to () and, if the flag is true,
-  prints its runtime*)
+(*Note start point for timing*)
+fun startTiming() = System.processtime ();
 
-fun cond_timeit flag f =
-  if flag then
-    let
-      val before = System.processtime ();
-      val result = f ();
-      val both = real (System.processtime () - before) / 10.0;
-    in
-      print ("Process time (incl GC): " ^ makestring both ^ " secs\n");
-      result
-    end
-  else f ();
+(*Finish timing and return string*)
+fun endTiming before = 
+  "User + GC: " ^ 
+  makestring (real (System.processtime () - before) / 10.0) ^ 
+  " secs";
 
 
 (* toplevel pretty printing (see also Pure/install_pp.ML) *)
diff -r e72cba5af6c5 -r 7211ea5f29e2 src/Pure/ML-Systems/smlnj-1.09.ML
--- a/src/Pure/ML-Systems/smlnj-1.09.ML	Fri Nov 28 10:54:13 1997 +0100
+++ b/src/Pure/ML-Systems/smlnj-1.09.ML	Fri Nov 28 10:59:14 1997 +0100
@@ -39,25 +39,24 @@
 Compiler.Control.secondaryPrompt := "# ";
 
 
-(* timing *)
+(** Compiler-independent timing functions **)
+
+(*Note start point for timing*)
+fun startTiming() = 
+  let val CPUtimer = Timer.startCPUTimer();
+      val time = Timer.checkCPUTimer(CPUtimer)
+  in  (CPUtimer,time)  end;
 
-(*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 open Time  (*...for Time.toString, Time.+ and Time.- *)
-	val CPUtimer = Timer.startCPUTimer();
-        val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer);
-        val result = f();
-        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 ();
+(*Finish timing and return string*)
+fun endTiming (CPUtimer, {gc,sys,usr}) =
+  let open Time  (*...for Time.toString, Time.+ and Time.- *)
+      val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
+  in  "User " ^ toString (usr2-usr) ^
+      "  GC " ^ toString (gc2-gc) ^
+      "  All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^
+      " secs"
+      handle Time => ""
+  end;
 
 
 (* toplevel pretty printing (see also Pure/install_pp.ML) *)
diff -r e72cba5af6c5 -r 7211ea5f29e2 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Nov 28 10:54:13 1997 +0100
+++ b/src/Pure/library.ML	Fri Nov 28 10:59:14 1997 +0100
@@ -802,6 +802,17 @@
 
 (** timing **)
 
+(*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 val start = startTiming()
+        val result = f ()
+    in
+	writeln (endTiming start);  result
+    end
+  else f ();
+
 (*unconditional timing function*)
 fun timeit x = cond_timeit true x;