src/Pure/Thy/export.scala
changeset 68167 327bb0f5f768
parent 68166 021c6fecaf5c
child 68171 13162bb3a677
     1.1 --- a/src/Pure/Thy/export.scala	Sun May 13 16:05:29 2018 +0200
     1.2 +++ b/src/Pure/Thy/export.scala	Sun May 13 16:26:01 2018 +0200
     1.3 @@ -63,14 +63,13 @@
     1.4      session_name: String,
     1.5      theory_name: String,
     1.6      name: String,
     1.7 -    compressed: Boolean,
     1.8 -    body: Future[Bytes])
     1.9 +    body: Future[(Boolean, Bytes)])
    1.10    {
    1.11      override def toString: String = compound_name(theory_name, name)
    1.12  
    1.13      def write(db: SQL.Database)
    1.14      {
    1.15 -      val bytes = body.join
    1.16 +      val (compressed, bytes) = body.join
    1.17        db.using_statement(Data.table.insert())(stmt =>
    1.18        {
    1.19          stmt.string(1) = session_name
    1.20 @@ -82,8 +81,11 @@
    1.21        })
    1.22      }
    1.23  
    1.24 -    def body_uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =
    1.25 -      if (compressed) body.join.uncompress(cache = cache) else body.join
    1.26 +    def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =
    1.27 +    {
    1.28 +      val (compressed, bytes) = body.join
    1.29 +      if (compressed) bytes.uncompress(cache = cache) else bytes
    1.30 +    }
    1.31    }
    1.32  
    1.33    def make_regex(pattern: String): Regex =
    1.34 @@ -114,8 +116,9 @@
    1.35    def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes,
    1.36      cache: XZ.Cache = XZ.cache()): Entry =
    1.37    {
    1.38 -    Entry(session_name, args.theory_name, args.name, args.compress,
    1.39 -      if (args.compress) Future.fork(body.compress(cache = cache)) else Future.value(body))
    1.40 +    Entry(session_name, args.theory_name, args.name,
    1.41 +      if (args.compress) Future.fork(body.maybe_compress(cache = cache))
    1.42 +      else Future.value((false, body)))
    1.43    }
    1.44  
    1.45    def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry =
    1.46 @@ -129,7 +132,7 @@
    1.47        if (res.next()) {
    1.48          val compressed = res.bool(Data.compressed)
    1.49          val body = res.bytes(Data.body)
    1.50 -        Entry(session_name, theory_name, name, compressed, Future.value(body))
    1.51 +        Entry(session_name, theory_name, name, Future.value(compressed, body))
    1.52        }
    1.53        else error(message("Bad export", theory_name, name))
    1.54      })
    1.55 @@ -275,7 +278,7 @@
    1.56  
    1.57              progress.echo("exporting " + path)
    1.58              Isabelle_System.mkdirs(path.dir)
    1.59 -            Bytes.write(path, entry.body_uncompressed(cache = xz_cache))
    1.60 +            Bytes.write(path, entry.uncompressed(cache = xz_cache))
    1.61            }
    1.62          }
    1.63        }