equal
deleted
inserted
replaced
12 structure Build: BUILD = |
12 structure Build: BUILD = |
13 struct |
13 struct |
14 |
14 |
15 (* command timings *) |
15 (* command timings *) |
16 |
16 |
17 type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name * time *) |
17 type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name, time*) |
18 |
18 |
19 val empty_timings: timings = Symtab.empty; |
19 val empty_timings: timings = Symtab.empty; |
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 |