equal
deleted
inserted
replaced
34 val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *) |
34 val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *) |
35 val some_preplay_time = (true, Time.zeroTime) (* > 0 ms *) |
35 val some_preplay_time = (true, Time.zeroTime) (* > 0 ms *) |
36 |
36 |
37 fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2)) |
37 fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2)) |
38 |
38 |
39 val string_of_preplay_time = ATP_Util.string_from_ext_time |
39 val string_of_preplay_time = ATP_Util.string_of_ext_time |
40 |
40 |
41 (* preplay tracing *) |
41 (* preplay tracing *) |
42 fun preplay_trace ctxt assms concl time = |
42 fun preplay_trace ctxt assms concl time = |
43 let |
43 let |
44 val ctxt = ctxt |> Config.put show_markup true |
44 val ctxt = ctxt |> Config.put show_markup true |