equal
deleted
inserted
replaced
103 fun timeit e = cond_timeit true "" e; |
103 fun timeit e = cond_timeit true "" e; |
104 fun timeap f x = timeit (fn () => f x); |
104 fun timeap f x = timeit (fn () => f x); |
105 fun timeap_msg msg f x = cond_timeit true msg (fn () => f x); |
105 fun timeap_msg msg f x = cond_timeit true msg (fn () => f x); |
106 |
106 |
107 fun protocol_message props t = |
107 fun protocol_message props t = |
108 Output.try_protocol_message (props @ Markup.timing_properties t) ""; |
108 Output.try_protocol_message (props @ Markup.timing_properties t) []; |
109 |
109 |
110 fun protocol props f x = |
110 fun protocol props f x = |
111 let |
111 let |
112 val (t, result) = timing (Exn.interruptible_capture f) x; |
112 val (t, result) = timing (Exn.interruptible_capture f) x; |
113 val _ = protocol_message props t; |
113 val _ = protocol_message props t; |