clarified implicit compression;
authorwenzelm
Sun May 13 16:26:01 2018 +0200 (12 months ago)
changeset 68167327bb0f5f768
parent 68166 021c6fecaf5c
child 68168 a9b49430f061
clarified implicit compression;
src/Pure/General/bytes.scala
src/Pure/Thy/export.ML
src/Pure/Thy/export.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Pure/General/bytes.scala	Sun May 13 16:05:29 2018 +0200
     1.2 +++ b/src/Pure/General/bytes.scala	Sun May 13 16:26:01 2018 +0200
     1.3 @@ -205,4 +205,11 @@
     1.4      using(new XZOutputStream(result, options, cache))(write_stream(_))
     1.5      new Bytes(result.toByteArray, 0, result.size)
     1.6    }
     1.7 +
     1.8 +  def maybe_compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.cache())
     1.9 +    : (Boolean, Bytes) =
    1.10 +  {
    1.11 +    val compressed = compress(options = options, cache = cache)
    1.12 +    if (compressed.length < length) (true, compressed) else (false, this)
    1.13 +  }
    1.14  }
     2.1 --- a/src/Pure/Thy/export.ML	Sun May 13 16:05:29 2018 +0200
     2.2 +++ b/src/Pure/Thy/export.ML	Sun May 13 16:26:01 2018 +0200
     2.3 @@ -33,7 +33,7 @@
     2.4      name = check_name name,
     2.5      compress = compress} body;
     2.6  
     2.7 -fun export thy name body = gen_export (fold (Integer.add o size) body 0 > 60) thy name body;
     2.8 +val export = gen_export true;
     2.9  val export_raw = gen_export false;
    2.10  
    2.11  end;
     3.1 --- a/src/Pure/Thy/export.scala	Sun May 13 16:05:29 2018 +0200
     3.2 +++ b/src/Pure/Thy/export.scala	Sun May 13 16:26:01 2018 +0200
     3.3 @@ -63,14 +63,13 @@
     3.4      session_name: String,
     3.5      theory_name: String,
     3.6      name: String,
     3.7 -    compressed: Boolean,
     3.8 -    body: Future[Bytes])
     3.9 +    body: Future[(Boolean, Bytes)])
    3.10    {
    3.11      override def toString: String = compound_name(theory_name, name)
    3.12  
    3.13      def write(db: SQL.Database)
    3.14      {
    3.15 -      val bytes = body.join
    3.16 +      val (compressed, bytes) = body.join
    3.17        db.using_statement(Data.table.insert())(stmt =>
    3.18        {
    3.19          stmt.string(1) = session_name
    3.20 @@ -82,8 +81,11 @@
    3.21        })
    3.22      }
    3.23  
    3.24 -    def body_uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =
    3.25 -      if (compressed) body.join.uncompress(cache = cache) else body.join
    3.26 +    def uncompressed(cache: XZ.Cache = XZ.cache()): Bytes =
    3.27 +    {
    3.28 +      val (compressed, bytes) = body.join
    3.29 +      if (compressed) bytes.uncompress(cache = cache) else bytes
    3.30 +    }
    3.31    }
    3.32  
    3.33    def make_regex(pattern: String): Regex =
    3.34 @@ -114,8 +116,9 @@
    3.35    def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes,
    3.36      cache: XZ.Cache = XZ.cache()): Entry =
    3.37    {
    3.38 -    Entry(session_name, args.theory_name, args.name, args.compress,
    3.39 -      if (args.compress) Future.fork(body.compress(cache = cache)) else Future.value(body))
    3.40 +    Entry(session_name, args.theory_name, args.name,
    3.41 +      if (args.compress) Future.fork(body.maybe_compress(cache = cache))
    3.42 +      else Future.value((false, body)))
    3.43    }
    3.44  
    3.45    def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry =
    3.46 @@ -129,7 +132,7 @@
    3.47        if (res.next()) {
    3.48          val compressed = res.bool(Data.compressed)
    3.49          val body = res.bytes(Data.body)
    3.50 -        Entry(session_name, theory_name, name, compressed, Future.value(body))
    3.51 +        Entry(session_name, theory_name, name, Future.value(compressed, body))
    3.52        }
    3.53        else error(message("Bad export", theory_name, name))
    3.54      })
    3.55 @@ -275,7 +278,7 @@
    3.56  
    3.57              progress.echo("exporting " + path)
    3.58              Isabelle_System.mkdirs(path.dir)
    3.59 -            Bytes.write(path, entry.body_uncompressed(cache = xz_cache))
    3.60 +            Bytes.write(path, entry.uncompressed(cache = xz_cache))
    3.61            }
    3.62          }
    3.63        }
     4.1 --- a/src/Pure/Tools/server_commands.scala	Sun May 13 16:05:29 2018 +0200
     4.2 +++ b/src/Pure/Tools/server_commands.scala	Sun May 13 16:26:01 2018 +0200
     4.3 @@ -220,7 +220,7 @@
     4.4                      val matcher = Export.make_matcher(args.export_pattern)
     4.5                      for { entry <- result.exports(name) if matcher(entry.theory_name, entry.name) }
     4.6                      yield {
     4.7 -                      val (base64, body) = entry.body.join.maybe_base64
     4.8 +                      val (base64, body) = entry.uncompressed().maybe_base64
     4.9                        JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
    4.10                      }
    4.11                    }))))