src/Pure/ML/ml_profiling.ML
author wenzelm
Sat, 02 Apr 2016 22:46:12 +0200
changeset 62824 3498c66b5e55
parent 62508 d0b68218ea55
child 62945 c38c08889aa9
permissions -rw-r--r--
proper signature;

(*  Title:      Pure/ML/ml_profiling.ML
    Author:     Makarius

Profiling for Poly/ML 5.6.
*)

signature ML_PROFILING =
sig
  val profile_time: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
  val profile_time_thread: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
  val profile_allocations: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
end;

structure ML_Profiling: ML_PROFILING =
struct

fun profile_time pr f x =
  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;

fun profile_time_thread pr f x =
  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;

fun profile_allocations pr f x =
  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;

end;