# HG changeset patch
# User wenzelm
# Date 1592416010 -7200
# Node ID 107472ccc60ded21bd9c5596b8ce0262c0bfd893
# Parent  e1b262e7480ceb20d9a8de7410015cf80d8203af
avoid resource problems of JVM by too many parallel XZ compression tasks;

diff -r e1b262e7480c -r 107472ccc60d src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Tue Jun 16 08:41:39 2020 +0000
+++ b/src/Pure/Thy/export.scala	Wed Jun 17 19:46:50 2020 +0200
@@ -143,11 +143,19 @@
       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) Future.fork(body.maybe_compress(cache = cache))
+      if (args.compress) {
+        val result = Future.promise[(Boolean, Bytes)]
+        later.send(() => result.fulfill(body.maybe_compress(cache = cache)))
+        result
+      }
       else Future.value((false, body)))
   }