src/Pure/PIDE/session.scala

 
 class Session(_session_options: => Options, val resources: Resources) extends Document.Session
 {
   session =>
 
-  val xml_cache: XML.Cache = XML.Cache.make()
-  val xz_cache: XZ.Cache = XZ.Cache.make()
+  val cache: XML.Cache = XML.Cache.make()
 
   def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
     Command.Blobs_Info.none
 
 

           if (!handled) {
             msg.properties match {
               case Protocol.Command_Timing(props, state_id, timing) if prover.defined =>
                 command_timings.post(Session.Command_Timing(props))
                 val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
-                change_command(_.accumulate(state_id, xml_cache.elem(message), xml_cache))
+                change_command(_.accumulate(state_id, cache.elem(message), cache))
 
               case Markup.Theory_Timing(props) =>
                 theory_timings.post(Session.Theory_Timing(props))
 
               case Markup.Task_Statistics(props) =>
                 task_statistics.post(Session.Task_Statistics(props))
 
               case Protocol.Export(args)
               if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
                 val id = Value.Long.unapply(args.id.get).get
-                val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
+                val export = Export.make_entry("", args, msg.bytes, cache)
                 change_command(_.add_export(id, (args.serial, export)))
 
               case Protocol.Loading_Theory(node_name, id) =>
                 val blobs_info = build_blobs_info(node_name)
                 try { global_state.change(_.begin_theory(node_name, id, msg.text, blobs_info)) }

 
               case List(Markup.Commands_Accepted.PROPERTY) =>
                 msg.text match {
                   case Protocol.Commands_Accepted(ids) =>
                     ids.foreach(id =>
-                      change_command(_.accumulate(id, Protocol.Commands_Accepted.message, xml_cache)))
+                      change_command(_.accumulate(id, Protocol.Commands_Accepted.message, cache)))
                   case _ => bad_output()
                 }
 
               case List(Markup.Assign_Update.PROPERTY) =>
                 msg.text match {

             }
           }
         case _ =>
           output.properties match {
             case Position.Id(state_id) =>
-              change_command(_.accumulate(state_id, output.message, xml_cache))
+              change_command(_.accumulate(state_id, output.message, cache))
 
             case _ if output.is_init =>
               val init_ok =
                 try {
                   Isabelle_System.make_services(classOf[Session.Protocol_Handler])