back to parallel compression: full AFP build does require 16GB Java heap (reverting 107472ccc60d);
authorwenzelm
Fri, 19 Jun 2020 18:44:31 +0200
changeset 71963 3e7d89d9912e
parent 71962 23398ed3aecf
child 71964 235173749448
back to parallel compression: full AFP build does require 16GB Java heap (reverting 107472ccc60d);
src/Pure/Thy/export.scala
--- 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)))
   }