src/Pure/ML-Systems/smlnj.ML
changeset 30187 b92b3375e919
parent 29564 f8b933a62151
child 30619 0226c07352db
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Sun Mar 01 14:45:23 2009 +0100
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Sun Mar 01 16:21:33 2009 +0100
     1.3 @@ -59,18 +59,19 @@
     1.4  (* compiler-independent timing functions *)
     1.5  
     1.6  fun start_timing () =
     1.7 -  let val CPUtimer = Timer.startCPUTimer();
     1.8 -      val time = Timer.checkCPUTimer(CPUtimer)
     1.9 -  in  (CPUtimer,time)  end;
    1.10 +  let
    1.11 +    val timer = Timer.startCPUTimer ();
    1.12 +    val time = Timer.checkCPUTimer timer;
    1.13 +  in (timer, time) end;
    1.14  
    1.15 -fun end_timing (CPUtimer, {sys,usr}) =
    1.16 -  let open Time  (*...for Time.toString, Time.+ and Time.- *)
    1.17 -      val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
    1.18 -  in  "User " ^ toString (usr2-usr) ^
    1.19 -      "  All "^ toString (sys2-sys + usr2-usr) ^
    1.20 -      " secs"
    1.21 -      handle Time => ""
    1.22 -  end;
    1.23 +fun end_timing (timer, {sys, usr}) =
    1.24 +  let
    1.25 +    open Time;  (*...for Time.toString, Time.+ and Time.- *)
    1.26 +    val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
    1.27 +    val user = usr2 - usr;
    1.28 +    val all = user + sys2 - sys;
    1.29 +    val message = "User " ^ toString user ^ "  All "^ toString all ^ " secs" handle Time => "";
    1.30 +  in {message = message, user = user, all = all} end;
    1.31  
    1.32  fun check_timer timer =
    1.33    let