author | wenzelm |
Fri, 20 Nov 2015 21:52:05 +0100 | |
changeset 61715 | 5dc95d957569 |
child 61885 | acdfc76a6c33 |
permissions | -rw-r--r-- |
(* Title: Pure/ML-Systems/ml_profiling_polyml.ML Author: Makarius Profiling for Poly/ML. *) fun profile 0 f x = f x | profile n f x = let val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n; val res = Exn.capture f x; val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0; in Exn.release res end;