back to parallel compression: full AFP build does require 16GB Java heap (reverting 107472ccc60d);
--- a/src/Pure/Thy/export.scala Fri Jun 19 18:29:37 2020 +0200
+++ b/src/Pure/Thy/export.scala Fri Jun 19 18:44:31 2020 +0200
@@ -143,19 +143,11 @@
regex.pattern.matcher(compound_name(theory_name, name)).matches
}
- private lazy val later: Consumer_Thread[() => Unit] =
- Consumer_Thread.fork(name = "Export.later", daemon = true)(
- consume = (run: () => Unit) => { run(); true })
-
def make_entry(session_name: String, args: Protocol.Export.Args, body: Bytes,
cache: XZ.Cache = XZ.cache()): Entry =
{
Entry(session_name, args.theory_name, args.name, args.executable,
- if (args.compress) {
- val result = Future.promise[(Boolean, Bytes)]
- later.send(() => result.fulfill(body.maybe_compress(cache = cache)))
- result
- }
+ if (args.compress) Future.fork(body.maybe_compress(cache = cache))
else Future.value((false, body)))
}