# HG changeset patch
# User wenzelm
# Date 1618223529 -7200
# Node ID c5a390b9ae00e011156116ea8a9d97b02ac907a2
# Parent  c83152933579ef5b6ca3c0255042e411e4fb916c
clarified cache;

diff -r c83152933579 -r c5a390b9ae00 src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Mon Apr 12 12:16:49 2021 +0200
+++ b/src/Pure/PIDE/prover.scala	Mon Apr 12 12:32:09 2021 +0200
@@ -88,7 +88,7 @@
 
   private def protocol_output(props: Properties.T, chunks: List[Bytes]): Unit =
   {
-    receiver(new Prover.Protocol_Output(cache.props(props), chunks))
+    receiver(new Prover.Protocol_Output(props, chunks))
   }
 
   private def output(kind: String, props: Properties.T, body: XML.Body): Unit =
@@ -264,7 +264,7 @@
   private def message_output(stream: InputStream): Thread =
   {
     def decode_chunk(chunk: Bytes): XML.Body =
-      Symbol.decode_yxml_failsafe(chunk.text)
+      Symbol.decode_yxml_failsafe(chunk.text, cache = cache)
 
     val thread_name = "message_output"
     Isabelle_Thread.fork(name = thread_name) {
@@ -275,13 +275,9 @@
             case None => finished = true
             case Some(header :: chunks) =>
               decode_chunk(header) match {
-                case List(XML.Elem(Markup(name, props), Nil)) =>
-                  val kind = name.intern
+                case List(XML.Elem(Markup(kind, props), Nil)) =>
                   if (kind == Markup.PROTOCOL) protocol_output(props, chunks)
-                  else {
-                    val body = decode_chunk(Prover.the_chunk(chunks, name))
-                    output(kind, props, body)
-                  }
+                  else output(kind, props, decode_chunk(Prover.the_chunk(chunks, kind)))
                 case _ => Prover.bad_header(header.toString)
               }
             case Some(_) => Prover.bad_chunks()