src/Pure/Thy/export.scala
changeset 68289 c29fc61fb1b1
parent 68288 d20770229f99
child 68290 f1f5ccc85b25
--- 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))
           }
         }
       }