src/Pure/Thy/export.scala

     val regex = make_regex(pattern)
     (theory_name: String, name: String) =>
       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)))
   }
 
   def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String)
     : Option[Entry] =