equal
deleted
inserted
replaced
1 (* Title: Pure/RAW/ml_profiling_polyml.ML |
|
2 Author: Makarius |
|
3 |
|
4 Profiling for Poly/ML. |
|
5 *) |
|
6 |
|
7 structure ML_Profiling = |
|
8 struct |
|
9 |
|
10 local |
|
11 |
|
12 fun profile n f x = |
|
13 let |
|
14 val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n; |
|
15 val res = Exn.capture f x; |
|
16 val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0; |
|
17 in Exn.release res end; |
|
18 |
|
19 in |
|
20 |
|
21 fun profile_time (_: (int * string) list -> unit) f x = profile 1 f x; |
|
22 fun profile_time_thread (_: (int * string) list -> unit) f x = profile 6 f x; |
|
23 fun profile_allocations (_: (int * string) list -> unit) f x = profile 2 f x; |
|
24 |
|
25 end; |
|
26 |
|
27 end; |
|