# HG changeset patch
# User wenzelm
# Date 1489443860 -3600
# Node ID 102b8e092860c9c064a8435d5c48ac8874969200
# Parent  edd3f532e4e3f1181e6329cf7fe08035e31b7051
more explicit Session.xml_cache;

diff -r edd3f532e4e3 -r 102b8e092860 src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Mon Mar 13 23:14:44 2017 +0100
+++ b/src/Pure/PIDE/prover.scala	Mon Mar 13 23:24:20 2017 +0100
@@ -75,13 +75,12 @@
 
 abstract class Prover(
   receiver: Prover.Receiver,
+  xml_cache: XML.Cache,
   system_channel: System_Channel,
   system_process: Prover.System_Process) extends Protocol
 {
   /** receiver output **/
 
-  val xml_cache: XML.Cache = new XML.Cache()
-
   private def system_output(text: String)
   {
     receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
diff -r edd3f532e4e3 -r 102b8e092860 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Mon Mar 13 23:14:44 2017 +0100
+++ b/src/Pure/PIDE/session.scala	Mon Mar 13 23:24:20 2017 +0100
@@ -118,6 +118,8 @@
 {
   session =>
 
+  val xml_cache: XML.Cache = new XML.Cache()
+
 
   /* global flags */
 
@@ -391,7 +393,7 @@
 
               case Protocol.Command_Timing(state_id, timing) if prover.defined =>
                 val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
-                accumulate(state_id, prover.get.xml_cache.elem(message))
+                accumulate(state_id, xml_cache.elem(message))
 
               case Markup.Assign_Update =>
                 msg.text match {
diff -r edd3f532e4e3 -r 102b8e092860 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Mar 13 23:14:44 2017 +0100
+++ b/src/Pure/System/isabelle_process.scala	Mon Mar 13 23:24:20 2017 +0100
@@ -19,7 +19,7 @@
   {
     session.start(receiver =>
       Isabelle_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
-        receiver = receiver, store = store))
+        receiver = receiver, xml_cache = session.xml_cache, store = store))
   }
 
   def apply(
@@ -29,6 +29,7 @@
     dirs: List[Path] = Nil,
     modes: List[String] = Nil,
     receiver: Prover.Receiver = Console.println(_),
+    xml_cache: XML.Cache = new XML.Cache(),
     store: Sessions.Store = Sessions.store()): Isabelle_Process =
   {
     val channel = System_Channel()
@@ -40,13 +41,16 @@
       catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
     process.stdin.close
 
-    new Isabelle_Process(receiver, channel, process)
+    new Isabelle_Process(receiver, xml_cache, channel, process)
   }
 }
 
 class Isabelle_Process private(
-    receiver: Prover.Receiver, channel: System_Channel, process: Prover.System_Process)
-  extends Prover(receiver, channel, process)
+    receiver: Prover.Receiver,
+    xml_cache: XML.Cache,
+    channel: System_Channel,
+    process: Prover.System_Process)
+  extends Prover(receiver, xml_cache, channel, process)
 {
   def encode(s: String): String = Symbol.encode(s)
   def decode(s: String): String = Symbol.decode(s)
diff -r edd3f532e4e3 -r 102b8e092860 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Mon Mar 13 23:14:44 2017 +0100
+++ b/src/Pure/Tools/debugger.scala	Mon Mar 13 23:24:20 2017 +0100
@@ -154,9 +154,9 @@
         case Markup.Debugger_Output(thread_name) =>
           YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes))) match {
             case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
-              val message =
-                prover.xml_cache.elem(XML.Elem(Markup(Markup.message(name), props), body))
-              the_debugger.add_output(thread_name, i -> message)
+              val debugger = the_debugger
+              val message = XML.Elem(Markup(Markup.message(name), props), body)
+              debugger.add_output(thread_name, i -> debugger.session.xml_cache.elem(message))
               true
             case _ => false
           }
@@ -171,7 +171,7 @@
   }
 }
 
-class Debugger private(session: Session)
+class Debugger private(val session: Session)
 {
   /* debugger state */