| changeset 53709 | 84522727f9d3 |
| parent 52837 | fe1f6a1707f7 |
| child 54342 | fbcaa9f08879 |
| 53708:92aa282841f8 | 53709:84522727f9d3 |
|---|---|
73 end; |
73 end; |
74 |
74 |
75 |
75 |
76 (* ML runtime system *) |
76 (* ML runtime system *) |
77 |
77 |
78 val exception_trace = PolyML.exception_trace; |
78 fun print_exception_trace (_: exn -> string) = PolyML.exception_trace; |
79 val timing = PolyML.timing; |
79 val timing = PolyML.timing; |
80 val profiling = PolyML.profiling; |
80 val profiling = PolyML.profiling; |
81 |
81 |
82 fun profile 0 f x = f x |
82 fun profile 0 f x = f x |
83 | profile n f x = |
83 | profile n f x = |