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