tuned -- use XZ.Cache;
authorwenzelm
Sun May 13 16:05:29 2018 +0200 (12 months ago)
changeset 68166021c6fecaf5c
parent 68165 a7a2174ac014
child 68167 327bb0f5f768
tuned -- use XZ.Cache;
src/Pure/Thy/export.scala
     1.1 --- a/src/Pure/Thy/export.scala	Sun May 13 15:55:30 2018 +0200
     1.2 +++ b/src/Pure/Thy/export.scala	Sun May 13 16:05:29 2018 +0200
     1.3 @@ -82,8 +82,8 @@
     1.4        })
     1.5      }
     1.6  
     1.7 -    def body_uncompressed: Bytes =
     1.8 -      if (compressed) body.join.uncompress() else body.join
     1.9 +    def body_uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =
    1.10 +      if (compressed) body.join.uncompress(cache = cache) else body.join
    1.11    }
    1.12  
    1.13    def make_regex(pattern: String): Regex =
    1.14 @@ -111,10 +111,11 @@
    1.15        regex.pattern.matcher(compound_name(theory_name, name)).matches
    1.16    }
    1.17  
    1.18 -  def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes): Entry =
    1.19 +  def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes,
    1.20 +    cache: XZ.Cache = XZ.cache()): Entry =
    1.21    {
    1.22      Entry(session_name, args.theory_name, args.name, args.compress,
    1.23 -      if (args.compress) Future.fork(body.compress()) else Future.value(body))
    1.24 +      if (args.compress) Future.fork(body.compress(cache = cache)) else Future.value(body))
    1.25    }
    1.26  
    1.27    def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry =
    1.28 @@ -141,6 +142,8 @@
    1.29  
    1.30    class Consumer private[Export](db: SQL.Database)
    1.31    {
    1.32 +    val xz_cache = XZ.make_cache()
    1.33 +
    1.34      db.create_table(Data.table)
    1.35  
    1.36      private val export_errors = Synchronized[List[String]](Nil)
    1.37 @@ -160,7 +163,7 @@
    1.38          })
    1.39  
    1.40      def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit =
    1.41 -      consumer.send(make_entry(session_name, args, body))
    1.42 +      consumer.send(make_entry(session_name, args, body, cache = xz_cache))
    1.43  
    1.44      def shutdown(close: Boolean = false): List[String] =
    1.45      {
    1.46 @@ -262,6 +265,8 @@
    1.47  
    1.48          // export
    1.49          if (export_pattern != "") {
    1.50 +          val xz_cache = XZ.make_cache()
    1.51 +
    1.52            val matcher = make_matcher(export_pattern)
    1.53            for { (theory_name, name) <- export_names if matcher(theory_name, name) }
    1.54            {
    1.55 @@ -270,7 +275,7 @@
    1.56  
    1.57              progress.echo("exporting " + path)
    1.58              Isabelle_System.mkdirs(path.dir)
    1.59 -            Bytes.write(path, entry.body_uncompressed)
    1.60 +            Bytes.write(path, entry.body_uncompressed(cache = xz_cache))
    1.61            }
    1.62          }
    1.63        }