equal
deleted
inserted
replaced
1 (* Title: Pure/ML-Systems/ml_profiling_polyml-5.6.ML |
|
2 Author: Makarius |
|
3 |
|
4 Profiling for Poly/ML 5.6. |
|
5 *) |
|
6 |
|
7 structure ML_Profiling = |
|
8 struct |
|
9 |
|
10 fun profile_time pr f x = |
|
11 PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x; |
|
12 |
|
13 fun profile_time_thread pr f x = |
|
14 PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x; |
|
15 |
|
16 fun profile_allocations pr f x = |
|
17 PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x; |
|
18 |
|
19 end; |
|