[polyml] time measurement

All,

I have a few questions about timing...

1. Are the times printed by PolyML.timing `user' times or elapsed times? (I suspect the first but would like to check...)

2. Do any of these times include garbage collection?

3. Is there any way for an ML program to access these times, i.e. can they be bound (perhaps as a record) to an ML name? (Either at the top-level only or even within a program for time so far.)

4. If the utime component of Posix.ProcEnv.times () was used to measure sections of code within a program would this time include interludes for garbage collection? (Is the garbage collector a different process and therefore not counted in this `user' time?)

Thanks for any help, Phil.