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-5.6.ML Author: Makarius Profiling for Poly/ML 5.6. *) fun profile 0 f x = f x | profile n f x = let val mode = (case n of 1 => PolyML.Profiling.ProfileTime | 2 => PolyML.Profiling.ProfileAllocations | 3 => PolyML.Profiling.ProfileLongIntEmulation | 6 => PolyML.Profiling.ProfileTimeThisThread | _ => raise Fail ("Bad profile mode: " ^ Int.toString n)); in PolyML.Profiling.profile mode f x end;