add command timings (like document command status);
authorwenzelm
Tue Apr 09 21:22:15 2013 +0200 (2013-04-09 ago)
changeset 51666b97aeb018900
parent 51665 cba83c9f72b9
child 51667 354c23ef2784
add command timings (like document command status);
src/Pure/Tools/build.ML
     1.1 --- a/src/Pure/Tools/build.ML	Tue Apr 09 21:14:00 2013 +0200
     1.2 +++ b/src/Pure/Tools/build.ML	Tue Apr 09 21:22:15 2013 +0200
     1.3 @@ -21,7 +21,8 @@
     1.4  fun update_timings props =
     1.5    (case Markup.parse_command_timing_properties props of
     1.6      SOME ({file, offset, name}, time) =>
     1.7 -      Symtab.map_default (file, Inttab.empty) (Inttab.update (offset, (name, time)))
     1.8 +      Symtab.map_default (file, Inttab.empty)
     1.9 +        (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, Time.+ (t, time))))
    1.10    | NONE => I);
    1.11  
    1.12  fun approximative_id name pos =