# HG changeset patch
# User wenzelm
# Date 1527346323 -7200
# Node ID c29fc61fb1b1950ede6cf276a3e04fda8d3fb8eb
# Parent  d20770229f9964907a0fc0f387c73af82083dd85
clarified cache;

diff -r d20770229f99 -r c29fc61fb1b1 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat May 26 13:36:28 2018 +0200
+++ b/src/Pure/Thy/export.scala	Sat May 26 16:52:03 2018 +0200
@@ -153,12 +153,10 @@
 
   /* database consumer thread */
 
-  def consumer(db: SQL.Database): Consumer = new Consumer(db)
+  def consumer(db: SQL.Database, cache: XZ.Cache = XZ.cache()): Consumer = new Consumer(db, cache)
 
-  class Consumer private[Export](db: SQL.Database)
+  class Consumer private[Export](db: SQL.Database, cache: XZ.Cache)
   {
-    val xz_cache = XZ.make_cache()
-
     private val export_errors = Synchronized[List[String]](Nil)
 
     private val consumer =
@@ -176,7 +174,7 @@
         })
 
     def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit =
-      consumer.send(make_entry(session_name, args, body, cache = xz_cache))
+      consumer.send(make_entry(session_name, args, body, cache = cache))
 
     def shutdown(close: Boolean = false): List[String] =
     {
@@ -210,8 +208,6 @@
 
         // 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)
@@ -220,7 +216,7 @@
             val path = export_dir + Path.basic(theory_name) + Path.explode(name)
             progress.echo("exporting " + path)
             Isabelle_System.mkdirs(path.dir)
-            Bytes.write(path, entry.uncompressed(cache = xz_cache))
+            Bytes.write(path, entry.uncompressed(cache = store.xz_cache))
           }
         }
       }
diff -r d20770229f99 -r c29fc61fb1b1 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat May 26 13:36:28 2018 +0200
+++ b/src/Pure/Tools/build.scala	Sat May 26 16:52:03 2018 +0200
@@ -189,7 +189,8 @@
     isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
 
     private val export_tmp_dir = Isabelle_System.tmp_dir("export")
-    private val export_consumer = Export.consumer(store.open_database(name, output = true))
+    private val export_consumer =
+      Export.consumer(store.open_database(name, output = true), cache = store.xz_cache)
 
     private val future_result: Future[Process_Result] =
       Future.thread("build") {