diff -r 098f3cf6c809 -r 080ef458f21a src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Apr 09 20:27:27 2013 +0200
+++ b/src/Pure/System/session.scala	Tue Apr 09 20:34:15 2013 +0200
@@ -323,8 +323,8 @@
           accumulate(state_id, output.message)
 
         case Markup.Command_Timing(state_id, timing) if output.is_protocol =>
-          // FIXME XML.cache (!?)
-          accumulate(state_id, XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))))
+          val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
+          accumulate(state_id, prover.get.xml_cache.elem(message))
 
         case Markup.Assign_Execs if output.is_protocol =>
           XML.content(output.body) match {