--- 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))
}
}
}