tuned -- use XZ.Cache;
authorwenzelm
Sun, 13 May 2018 16:33:11 +0200
changeset 68168 a9b49430f061
parent 68167 327bb0f5f768
child 68169 395432e7516e
tuned -- use XZ.Cache;
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 {