1(* Title: Pure/ML/ml_profiling.ML 2 Author: Makarius 3 4ML profiling. 5*) 6 7signature ML_PROFILING = 8sig 9 val profile_time: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b 10 val profile_time_thread: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b 11 val profile_allocations: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b 12end; 13 14structure ML_Profiling: ML_PROFILING = 15struct 16 17fun profile_time pr f x = 18 PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x; 19 20fun profile_time_thread pr f x = 21 PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x; 22 23fun profile_allocations pr f x = 24 PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x; 25 26end; 27