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