equal
deleted
inserted
replaced
79 else if function = Markup.command_timing then |
79 else if function = Markup.command_timing then |
80 let |
80 let |
81 val name = the_default "" (Properties.get args Markup.nameN); |
81 val name = the_default "" (Properties.get args Markup.nameN); |
82 val pos = Position.of_properties args; |
82 val pos = Position.of_properties args; |
83 val {elapsed, ...} = Markup.parse_timing_properties args; |
83 val {elapsed, ...} = Markup.parse_timing_properties args; |
|
84 val is_significant = |
|
85 Timing.is_relevant_time elapsed andalso |
|
86 Time.>= (elapsed, Options.default_seconds "command_timing_threshold"); |
84 in |
87 in |
85 if Timing.is_relevant_time elapsed then |
88 if is_significant then |
86 (case approximative_id name pos of |
89 (case approximative_id name pos of |
87 SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed) |
90 SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed) |
88 | NONE => ()) |
91 | NONE => ()) |
89 else () |
92 else () |
90 end |
93 end |