changeset 14979 | 245955f0c579 |
parent 14519 | 4ca3608fdf4f |
--- a/src/Pure/ML-Systems/cpu-timer-basis.ML Sun Jun 20 09:27:40 2004 +0200 +++ b/src/Pure/ML-Systems/cpu-timer-basis.ML Sun Jun 20 09:28:35 2004 +0200 @@ -21,3 +21,8 @@ handle Time => "" end; +fun checkTimer timer = + let + val {sys, usr} = Timer.checkCPUTimer timer; + val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *) + in (sys, usr, gc) end;