equal
deleted
inserted
replaced
20 |
20 |
21 fun update_timings props = |
21 fun update_timings props = |
22 (case Markup.parse_command_timing_properties props of |
22 (case Markup.parse_command_timing_properties props of |
23 SOME ({file, offset, name}, time) => |
23 SOME ({file, offset, name}, time) => |
24 Symtab.map_default (file, Inttab.empty) |
24 Symtab.map_default (file, Inttab.empty) |
25 (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, Time.+ (t, time)))) |
25 (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time))) |
26 | NONE => I); |
26 | NONE => I); |
27 |
27 |
28 fun approximative_id name pos = |
28 fun approximative_id name pos = |
29 (case (Position.file_of pos, Position.offset_of pos) of |
29 (case (Position.file_of pos, Position.offset_of pos) of |
30 (SOME file, SOME offset) => |
30 (SOME file, SOME offset) => |
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 = |
84 val is_significant = |
85 Timing.is_relevant_time elapsed andalso |
85 Timing.is_relevant_time elapsed andalso |
86 Time.>= (elapsed, Options.default_seconds "command_timing_threshold"); |
86 elapsed >= Options.default_seconds "command_timing_threshold"; |
87 in |
87 in |
88 if is_significant then |
88 if is_significant then |
89 (case approximative_id name pos of |
89 (case approximative_id name pos of |
90 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) |
91 | NONE => ()) |
91 | NONE => ()) |