src/Pure/ML-Systems/polyml_common.ML

 exception Interrupt = SML90.Interrupt;
 
 use "ML-Systems/exn.ML";
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
+use "ML-Systems/timing.ML";
 use "ML-Systems/system_shell.ML";
 use "ML-Systems/ml_pretty.ML";
 use "ML-Systems/use_context.ML";
 
 

 
 val ord = SML90.ord;
 val chr = SML90.chr;
 val explode = SML90.explode;
 val implode = SML90.implode;
-
-
-(* compiler-independent timing functions *)
-
-fun start_timing () =
-  let
-    val timer = Timer.startCPUTimer ();
-    val time = Timer.checkCPUTimer timer;
-  in (timer, time) end;
-
-fun end_timing (timer, {sys, usr}) =
-  let
-    open Time;  (*...for Time.toString, Time.+ and Time.- *)
-    val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
-    val user = usr2 - usr;
-    val all = user + sys2 - sys;
-    val message = "User " ^ toString user ^ "  All "^ toString all ^ " secs" handle Time => "";
-  in {message = message, user = user, all = all} end;
-
-fun check_timer timer =
-  let
-    val {sys, usr} = Timer.checkCPUTimer timer;
-    val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
-  in (sys, usr, gc) end;
 
 
 (* prompts *)
 
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);