src/Pure/ML/ml_profiling.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 62945 c38c08889aa9
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      Pure/ML/ml_profiling.ML
     2     Author:     Makarius
     3 
     4 ML profiling.
     5 *)
     6 
     7 signature ML_PROFILING =
     8 sig
     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
    12 end;
    13 
    14 structure ML_Profiling: ML_PROFILING =
    15 struct
    16 
    17 fun profile_time pr f x =
    18   PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
    19 
    20 fun profile_time_thread pr f x =
    21   PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
    22 
    23 fun profile_allocations pr f x =
    24   PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
    25 
    26 end;