--- 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*)
--- 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) *)
--- 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) *)
--- 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;