45 |
45 |
46 |
46 |
47 (* compiler-independent timing functions *) |
47 (* compiler-independent timing functions *) |
48 |
48 |
49 fun start_timing () = |
49 fun start_timing () = |
50 let val CPUtimer = Timer.startCPUTimer(); |
50 let |
51 val time = Timer.checkCPUTimer(CPUtimer) |
51 val timer = Timer.startCPUTimer (); |
52 in (CPUtimer,time) end; |
52 val time = Timer.checkCPUTimer timer; |
|
53 in (timer, time) end; |
53 |
54 |
54 fun end_timing (CPUtimer, {sys,usr}) = |
55 fun end_timing (timer, {sys, usr}) = |
55 let open Time (*...for Time.toString, Time.+ and Time.- *) |
56 let |
56 val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer) |
57 open Time; (*...for Time.toString, Time.+ and Time.- *) |
57 in "User " ^ toString (usr2-usr) ^ |
58 val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer; |
58 " All "^ toString (sys2-sys + usr2-usr) ^ |
59 val user = usr2 - usr; |
59 " secs" |
60 val all = user + sys2 - sys; |
60 handle Time => "" |
61 val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => ""; |
61 end; |
62 in {message = message, user = user, all = all} end; |
62 |
63 |
63 fun check_timer timer = |
64 fun check_timer timer = |
64 let |
65 let |
65 val {sys, usr} = Timer.checkCPUTimer timer; |
66 val {sys, usr} = Timer.checkCPUTimer timer; |
66 val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *) |
67 val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *) |