src/Pure/Thy/export.scala

--- a/src/Pure/Thy/export.scala	Sat Dec 31 14:58:34 2022 +0100
+++ b/src/Pure/Thy/export.scala	Sat Dec 31 15:32:12 2022 +0100
@@ -107,13 +107,36 @@
   def message(msg: String, theory_name: String, name: String): String =
     msg + " " + quote(name) + " for theory " + quote(theory_name)
 
-  def empty_entry(theory_name: String, name: String): Entry =
-    Entry(Entry_Name(theory = theory_name, name = name),
-      false, Future.value(false, Bytes.empty), XML.Cache.none)
+  object Entry {
+    def apply(
+      entry_name: Entry_Name,
+      executable: Boolean,
+      body: Future[(Boolean, Bytes)],
+      cache: XML.Cache
+    ): Entry = new Entry(entry_name, executable, body, cache)
+
+    def empty(theory_name: String, name: String): Entry =
+      Entry(Entry_Name(theory = theory_name, name = name),
+        false, Future.value(false, Bytes.empty), XML.Cache.none)
 
-  sealed case class Entry(
-    entry_name: Entry_Name,
-    executable: Boolean,
+    def make(
+      session_name: String,
+      args: Protocol.Export.Args,
+      bytes: Bytes,
+      cache: XML.Cache
+    ): Entry = {
+      val body =
+        if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.compress))
+        else Future.value((false, bytes))
+      val entry_name =
+        Entry_Name(session = session_name, theory = args.theory_name, name = args.name)
+      Entry(entry_name, args.executable, body, cache)
+    }
+  }
+
+  final class Entry private(
+    val entry_name: Entry_Name,
+    val executable: Boolean,
     body: Future[(Boolean, Bytes)],
     cache: XML.Cache
   ) {
@@ -122,6 +145,9 @@
     def name: String = entry_name.name
     override def toString: String = name
 
+    def is_finished: Boolean = body.is_finished
+    def cancel(): Unit = body.cancel()
+
     def compound_name: String = entry_name.compound_name
 
     def name_has_prefix(s: String): Boolean = name.startsWith(s)
@@ -176,19 +202,6 @@
     (entry_name: Entry_Name) => regs.exists(_.matches(entry_name.compound_name))
   }
 
-  def make_entry(
-    session_name: String,
-    args: Protocol.Export.Args,
-    bytes: Bytes,
-    cache: XML.Cache
-  ): Entry = {
-    val body =
-      if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.compress))
-      else Future.value((false, bytes))
-    val entry_name = Entry_Name(session = session_name, theory = args.theory_name, name = args.name)
-    Entry(entry_name, args.executable, body, cache)
-  }
-
 
   /* database consumer thread */
 
@@ -200,7 +213,7 @@
 
     private val consumer =
       Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")(
-        bulk = { case (entry, _) => entry.body.is_finished },
+        bulk = { case (entry, _) => entry.is_finished },
         consume =
           { (args: List[(Entry, Boolean)]) =>
             val results =
@@ -208,7 +221,7 @@
                 for ((entry, strict) <- args)
                 yield {
                   if (progress.stopped) {
-                    entry.body.cancel()
+                    entry.cancel()
                     Exn.Res(())
                   }
                   else if (entry.entry_name.readable(db)) {
@@ -227,7 +240,7 @@
     def make_entry(session_name: String, args0: Protocol.Export.Args, body: Bytes): Unit = {
       if (!progress.stopped && !body.is_empty) {
         val args = if (db.is_server) args0.copy(compress = false) else args0
-        consumer.send(Export.make_entry(session_name, args, body, cache) -> args.strict)
+        consumer.send(Entry.make(session_name, args, body, cache) -> args.strict)
       }
     }
 
@@ -403,7 +416,7 @@
 
     def apply(theory: String, name: String, permissive: Boolean = false): Entry =
       get(theory, name) match {
-        case None if permissive => empty_entry(theory, name)
+        case None if permissive => Entry.empty(theory, name)
         case None => error("Missing export entry " + quote(compound_name(theory, name)))
         case Some(entry) => entry
       }