author | wenzelm |
Sat, 02 Apr 2016 22:46:12 +0200 | |
changeset 62824 | 3498c66b5e55 |
parent 62508 | d0b68218ea55 |
child 62945 | c38c08889aa9 |
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 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
4 |
Profiling for Poly/ML 5.6. |
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; |