[polyml] profiling details

Hi,

im an Isabelle Developer, wondering about the details of profiling 1&2: * what happens if another thread is executing while profiling is active for a selected thread (lets say by calling profile 1 f x in Isabelle)? In the resulting profile it looks to me like profiling doesnt know about threads and just accumulates all timings while active. Is this the same situation for profiling 1 and 2? * is it possible or even wise to reduce the distance of profiling 1"ticks" to achieve more accurate timings? * if a call gets "credit" for an allocation in a profiling 2 log, was the allocation done while profling 2 was active, or did it become garbage while profling 2 was active?

Regards, Andy