| author | paulson <lp15@cam.ac.uk> |
| Tue, 19 Sep 2017 16:37:19 +0100 | |
| changeset 66660 | bc3584f7ac0c |
| parent 62945 | c38c08889aa9 |
| child 73834 | 364bac6691de |
| permissions | -rw-r--r-- |
|
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 | 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 | 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 = |
|
|
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; |