# HG changeset patch
# User wenzelm
# Date 1526220329 -7200
# Node ID 021c6fecaf5c5d2b721ff26d6eacdccec7759dd6
# Parent  a7a2174ac01491b29b8cad1802bdd9f7a382876f
tuned -- use XZ.Cache;

diff -r a7a2174ac014 -r 021c6fecaf5c src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sun May 13 15:55:30 2018 +0200
+++ b/src/Pure/Thy/export.scala	Sun May 13 16:05:29 2018 +0200
@@ -82,8 +82,8 @@
       })
     }
 
-    def body_uncompressed: Bytes =
-      if (compressed) body.join.uncompress() else body.join
+    def body_uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =
+      if (compressed) body.join.uncompress(cache = cache) else body.join
   }
 
   def make_regex(pattern: String): Regex =
@@ -111,10 +111,11 @@
       regex.pattern.matcher(compound_name(theory_name, name)).matches
   }
 
-  def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes): Entry =
+  def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes,
+    cache: XZ.Cache = XZ.cache()): Entry =
   {
     Entry(session_name, args.theory_name, args.name, args.compress,
-      if (args.compress) Future.fork(body.compress()) else Future.value(body))
+      if (args.compress) Future.fork(body.compress(cache = cache)) else Future.value(body))
   }
 
   def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry =
@@ -141,6 +142,8 @@
 
   class Consumer private[Export](db: SQL.Database)
   {
+    val xz_cache = XZ.make_cache()
+
     db.create_table(Data.table)
 
     private val export_errors = Synchronized[List[String]](Nil)
@@ -160,7 +163,7 @@
         })
 
     def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit =
-      consumer.send(make_entry(session_name, args, body))
+      consumer.send(make_entry(session_name, args, body, cache = xz_cache))
 
     def shutdown(close: Boolean = false): List[String] =
     {
@@ -262,6 +265,8 @@
 
         // export
         if (export_pattern != "") {
+          val xz_cache = XZ.make_cache()
+
           val matcher = make_matcher(export_pattern)
           for { (theory_name, name) <- export_names if matcher(theory_name, name) }
           {
@@ -270,7 +275,7 @@
 
             progress.echo("exporting " + path)
             Isabelle_System.mkdirs(path.dir)
-            Bytes.write(path, entry.body_uncompressed)
+            Bytes.write(path, entry.body_uncompressed(cache = xz_cache))
           }
         }
       }