tuned -- use XZ.Cache;
authorwenzelm
Sun May 13 16:33:11 2018 +0200 (12 months ago)
changeset 68168a9b49430f061
parent 68167 327bb0f5f768
child 68169 395432e7516e
tuned -- use XZ.Cache;
src/Pure/PIDE/session.scala
     1.1 --- a/src/Pure/PIDE/session.scala	Sun May 13 16:26:01 2018 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Sun May 13 16:33:11 2018 +0200
     1.3 @@ -119,6 +119,7 @@
     1.4    session =>
     1.5  
     1.6    val xml_cache: XML.Cache = new XML.Cache()
     1.7 +  val xz_cache: XZ.Cache = XZ.make_cache()
     1.8  
     1.9  
    1.10    /* global flags */
    1.11 @@ -436,8 +437,8 @@
    1.12                case Markup.Export(args)
    1.13                if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
    1.14                  val id = Value.Long.unapply(args.id.get).get
    1.15 -                val entry = (args.serial, Export.make_entry("", args, msg.bytes))
    1.16 -                change_command(_.add_export(id, entry))
    1.17 +                val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
    1.18 +                change_command(_.add_export(id, (args.serial, export)))
    1.19  
    1.20                case Markup.Assign_Update =>
    1.21                  msg.text match {