src/Pure/Thy/export.scala

--- a/src/Pure/Thy/export.scala	Mon Jun 26 22:45:04 2023 +0200
+++ b/src/Pure/Thy/export.scala	Mon Jun 26 23:20:32 2023 +0200
@@ -50,6 +50,37 @@
         Base.session_name.equal(session_name),
         if_proper(theory_name, Base.theory_name.equal(theory_name)),
         if_proper(name, Base.name.equal(name)))
+
+    def readable_entry(db: SQL.Database, entry_name: Entry_Name): Boolean = {
+      db.execute_query_statementB(
+        Data.Base.table.select(List(Base.name),
+          sql = where_equal(entry_name.session, entry_name.theory, entry_name.name)))
+    }
+
+    def read_entry(db: SQL.Database, entry_name: Entry_Name, cache: XML.Cache): Option[Entry] =
+      db.execute_query_statementO[Entry](
+        Data.Base.table.select(List(Data.Base.executable, Data.Base.compressed, Data.Base.body),
+          sql = Data.where_equal(entry_name.session, entry_name.theory, entry_name.name)),
+        { res =>
+          val executable = res.bool(Data.Base.executable)
+          val compressed = res.bool(Data.Base.compressed)
+          val bytes = res.bytes(Data.Base.body)
+          val body = Future.value(compressed, bytes)
+          Entry(entry_name, executable, body, cache)
+        }
+      )
+
+    def write_entry(db: SQL.Database, entry: Entry): Unit = {
+      val (compressed, bs) = entry.body.join
+      db.execute_statement(Base.table.insert(), body = { stmt =>
+        stmt.string(1) = entry.session_name
+        stmt.string(2) = entry.theory_name
+        stmt.string(3) = entry.name
+        stmt.bool(4) = entry.executable
+        stmt.bool(5) = compressed
+        stmt.bytes(6) = bs
+      })
+    }
   }
 
   def compound_name(a: String, b: String): String =
@@ -65,25 +96,6 @@
       }
       else Path.make(elems.drop(prune))
     }
-
-    def readable(db: SQL.Database): Boolean = {
-      db.execute_query_statementB(
-        Data.Base.table.select(List(Data.Base.name),
-          sql = Data.where_equal(session, theory, name)))
-    }
-
-    def read(db: SQL.Database, cache: XML.Cache): Option[Entry] =
-      db.execute_query_statementO[Entry](
-        Data.Base.table.select(List(Data.Base.executable, Data.Base.compressed, Data.Base.body),
-          sql = Data.where_equal(session, theory, name)),
-        { res =>
-          val executable = res.bool(Data.Base.executable)
-          val compressed = res.bool(Data.Base.compressed)
-          val bytes = res.bytes(Data.Base.body)
-          val body = Future.value(compressed, bytes)
-          Entry(this, executable, body, cache)
-        }
-      )
   }
 
   def read_theory_names(db: SQL.Database, session_name: String): List[String] =
@@ -138,8 +150,8 @@
   final class Entry private(
     val entry_name: Entry_Name,
     val executable: Boolean,
-    body: Future[(Boolean, Bytes)],
-    cache: XML.Cache
+    val body: Future[(Boolean, Bytes)],
+    val cache: XML.Cache
   ) {
     def session_name: String = entry_name.session
     def theory_name: String = entry_name.theory
@@ -165,19 +177,6 @@
     def text: String = bytes.text
 
     def yxml: XML.Body = YXML.parse_body(UTF8.decode_permissive(bytes), cache = cache)
-
-    def write(db: SQL.Database): Unit = {
-      val (compressed, bs) = body.join
-      db.execute_statement(Data.Base.table.insert(), body =
-        { stmt =>
-          stmt.string(1) = session_name
-          stmt.string(2) = theory_name
-          stmt.string(3) = name
-          stmt.bool(4) = executable
-          stmt.bool(5) = compressed
-          stmt.bytes(6) = bs
-        })
-    }
   }
 
   def make_regex(pattern: String): Regex = {
@@ -224,14 +223,14 @@
                     entry.cancel()
                     Exn.Res(())
                   }
-                  else if (entry.entry_name.readable(db)) {
+                  else if (Data.readable_entry(db, entry.entry_name)) {
                     if (strict) {
                       val msg = message("Duplicate export", entry.theory_name, entry.name)
                       errors.change(msg :: _)
                     }
                     Exn.Res(())
                   }
-                  else Exn.capture { entry.write(db) }
+                  else Exn.capture { Data.write_entry(db, entry) }
                 }
               }
             (results, true)
@@ -403,10 +402,10 @@
           entry <- snapshot.all_exports.get(entry_name)
         } yield entry
       def db_entry: Option[Entry] =
-        db_hierarchy.view.map(database =>
-          Export.Entry_Name(session = database.session, theory = theory, name = name)
-            .read(database.db, cache))
-          .collectFirst({ case Some(entry) => entry })
+        db_hierarchy.view.map { database =>
+          val entry_name = Export.Entry_Name(session = database.session, theory = theory, name = name)
+          Data.read_entry(database.db, entry_name, cache)
+        }.collectFirst({ case Some(entry) => entry })
 
       snapshot_entry orElse db_entry
     }
@@ -528,7 +527,7 @@
         val matcher = make_matcher(export_patterns)
         for {
           entry_name <- entry_names if matcher(entry_name)
-          entry <- entry_name.read(db, store.cache)
+          entry <- Data.read_entry(db, entry_name, store.cache)
         } {
           val path = export_dir + entry_name.make_path(prune = export_prune)
           progress.echo("export " + path + (if (entry.executable) " (executable)" else ""))