# HG changeset patch
# User wenzelm
# Date 1365535335 -7200
# Node ID b97aeb018900eaab7cb188e66164c3f9ee23b8ac
# Parent  cba83c9f72b96115c02b8b5eaa3171de35f7d7f2
add command timings (like document command status);

diff -r cba83c9f72b9 -r b97aeb018900 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Tue Apr 09 21:14:00 2013 +0200
+++ b/src/Pure/Tools/build.ML	Tue Apr 09 21:22:15 2013 +0200
@@ -21,7 +21,8 @@
 fun update_timings props =
   (case Markup.parse_command_timing_properties props of
     SOME ({file, offset, name}, time) =>
-      Symtab.map_default (file, Inttab.empty) (Inttab.update (offset, (name, time)))
+      Symtab.map_default (file, Inttab.empty)
+        (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, Time.+ (t, time))))
   | NONE => I);
 
 fun approximative_id name pos =