# HG changeset patch
# User wenzelm
# Date 1526221991 -7200
# Node ID a9b49430f0614b9225a9b2a929c5226d665da463
# Parent  327bb0f5f768202d0368ced8a034facfb7d056ca
tuned -- use XZ.Cache;

diff -r 327bb0f5f768 -r a9b49430f061 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sun May 13 16:26:01 2018 +0200
+++ b/src/Pure/PIDE/session.scala	Sun May 13 16:33:11 2018 +0200
@@ -119,6 +119,7 @@
   session =>
 
   val xml_cache: XML.Cache = new XML.Cache()
+  val xz_cache: XZ.Cache = XZ.make_cache()
 
 
   /* global flags */
@@ -436,8 +437,8 @@
               case Markup.Export(args)
               if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
                 val id = Value.Long.unapply(args.id.get).get
-                val entry = (args.serial, Export.make_entry("", args, msg.bytes))
-                change_command(_.add_export(id, entry))
+                val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
+                change_command(_.add_export(id, (args.serial, export)))
 
               case Markup.Assign_Update =>
                 msg.text match {