# HG changeset patch
# User wenzelm
# Date 1592585071 -7200
# Node ID 3e7d89d9912efa65db1af9689b9c8b797cf73712
# Parent  23398ed3aecfb177c197cafc22a9014c39da8ce1
back to parallel compression: full AFP build does require 16GB Java heap (reverting 107472ccc60d);

diff -r 23398ed3aecf -r 3e7d89d9912e 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)))
   }