# HG changeset patch
# User wenzelm
# Date 1365532455 -7200
# Node ID 080ef458f21ae39048e2e93a4bfb035581dd5339
# Parent  098f3cf6c809d9619cadfe5b8af78ba0373e2acc
public Isabelle_Process.xml_cache (thread-safe);
cache derived status messages;

diff -r 098f3cf6c809 -r 080ef458f21a src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Tue Apr 09 20:27:27 2013 +0200
+++ b/src/Pure/System/isabelle_process.scala	Tue Apr 09 20:34:15 2013 +0200
@@ -82,13 +82,13 @@
 
   /* output */
 
+  val xml_cache = new XML.Cache()
+
   private def system_output(text: String)
   {
     receiver(new Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
   }
 
-  private val xml_cache = new XML.Cache()
-
   private def output_message(kind: String, props: Properties.T, body: XML.Body)
   {
     if (kind == Markup.INIT) system_channel.accepted()
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 {