--- a/src/Pure/ML-Systems/mosml.ML Sun Apr 04 15:34:14 2004 +0200
+++ b/src/Pure/ML-Systems/mosml.ML Mon Apr 05 13:23:10 2004 +0200
@@ -58,22 +58,7 @@
load "Timer";
-(*Note start point for timing*)
-fun startTiming() =
- let val CPUtimer = Timer.startCPUTimer();
- val time = Timer.checkCPUTimer(CPUtimer)
- in (CPUtimer,time) end;
-
-(*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;
+use "ML-Systems/cpu-timer-gc.ML";
(* ML command execution *)