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 if is_relevant t then |
|
109 Output.try_protocol_message (props @ Markup.timing_properties t) [] |
|
110 else (); |
109 |
111 |
110 fun protocol props f x = |
112 fun protocol props f x = |
111 let |
113 let |
112 val (t, result) = timing (Exn.interruptible_capture f) x; |
114 val (t, result) = timing (Exn.interruptible_capture f) x; |
113 val _ = protocol_message props t; |
115 val _ = protocol_message props t; |