| author | Manuel Eberl <eberlm@in.tum.de> |
| Tue, 19 Jan 2016 11:19:25 +0100 | |
| changeset 62201 | eca7b38c8ee5 |
| parent 61925 | ab52f183f020 |
| permissions | -rw-r--r-- |
| 61925 | 1 |
(* Title: Pure/RAW/ml_profiling_polyml-5.6.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 |
|
|
61885
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
7 |
structure ML_Profiling = |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
8 |
struct |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
9 |
|
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
10 |
fun profile_time pr f x = |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
11 |
PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x; |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
12 |
|
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
13 |
fun profile_time_thread pr f x = |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
14 |
PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x; |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
15 |
|
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
16 |
fun profile_allocations pr f x = |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
17 |
PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x; |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
18 |
|
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
19 |
end; |