equal
deleted
inserted
replaced
152 val user = usr2 - usr + gc2 - gc; |
152 val user = usr2 - usr + gc2 - gc; |
153 val all = user + sys2 - sys; |
153 val all = user + sys2 - sys; |
154 val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => ""; |
154 val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => ""; |
155 in {message = message, user = user, all = all} end; |
155 in {message = message, user = user, all = all} end; |
156 |
156 |
157 fun check_timer timer = |
|
158 let val {sys, usr, gc} = Timer.checkCPUTimer timer |
|
159 in (sys, usr, gc) end; |
|
160 |
|
161 |
157 |
162 (* SML basis library fixes *) |
158 (* SML basis library fixes *) |
163 |
159 |
164 structure TextIO = |
160 structure TextIO = |
165 struct |
161 struct |