isabelle: src/Pure/ML/ml_profiling.ML@c1b63124245c (annotated)

62508 d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	1	(* Title: Pure/ML/ml_profiling.ML
61715 5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	2	Author: Makarius
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	3
62945 c38c08889aa9 tuned comments; wenzelm parents: 62824 diff changeset	4	ML profiling.
61715 5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	5	*)
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; wenzelm parents: diff changeset	6
62824 3498c66b5e55 proper signature; wenzelm parents: 62508 diff changeset	7	signature ML_PROFILING =
3498c66b5e55 proper signature; wenzelm parents: 62508 diff changeset	8	sig
3498c66b5e55 proper signature; wenzelm parents: 62508 diff changeset	9	val profile_time: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
3498c66b5e55 proper signature; wenzelm parents: 62508 diff changeset	10	val profile_time_thread: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
3498c66b5e55 proper signature; wenzelm parents: 62508 diff changeset	11	val profile_allocations: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
3498c66b5e55 proper signature; wenzelm parents: 62508 diff changeset	12	end;
3498c66b5e55 proper signature; wenzelm parents: 62508 diff changeset	13
3498c66b5e55 proper signature; wenzelm parents: 62508 diff changeset	14	structure ML_Profiling: ML_PROFILING =
61885 acdfc76a6c33 more explicit ML profiling, with official Isabelle output; wenzelm parents: 61715 diff changeset	15	struct
acdfc76a6c33 more explicit ML profiling, with official Isabelle output; wenzelm parents: 61715 diff changeset	16
acdfc76a6c33 more explicit ML profiling, with official Isabelle output; wenzelm parents: 61715 diff changeset	17	fun profile_time pr f x =
acdfc76a6c33 more explicit ML profiling, with official Isabelle output; wenzelm parents: 61715 diff changeset	18	PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
acdfc76a6c33 more explicit ML profiling, with official Isabelle output; wenzelm parents: 61715 diff changeset	19
acdfc76a6c33 more explicit ML profiling, with official Isabelle output; wenzelm parents: 61715 diff changeset	20	fun profile_time_thread pr f x =
acdfc76a6c33 more explicit ML profiling, with official Isabelle output; wenzelm parents: 61715 diff changeset	21	PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
acdfc76a6c33 more explicit ML profiling, with official Isabelle output; wenzelm parents: 61715 diff changeset	22
acdfc76a6c33 more explicit ML profiling, with official Isabelle output; wenzelm parents: 61715 diff changeset	23	fun profile_allocations pr f x =
acdfc76a6c33 more explicit ML profiling, with official Isabelle output; wenzelm parents: 61715 diff changeset	24	PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
acdfc76a6c33 more explicit ML profiling, with official Isabelle output; wenzelm parents: 61715 diff changeset	25
acdfc76a6c33 more explicit ML profiling, with official Isabelle output; wenzelm parents: 61715 diff changeset	26	end;

author	nipkow
	Tue, 05 Nov 2019 14:57:41 +0100
changeset 71033	c1b63124245c
parent 62945	c38c08889aa9
child 73834	364bac6691de
permissions	-rw-r--r--