# HG changeset patch
# User wenzelm
# Date 1657539368 -7200
# Node ID 88598f7c961439f17e501807de70ae1a19d87e7e
# Parent  ca8ae1ffd2b8d6071dc94c07f8ec1980479393c3
clarified signature;

diff -r ca8ae1ffd2b8 -r 88598f7c9614 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Mon Jul 11 13:21:22 2022 +0200
+++ b/src/Pure/Thy/export.scala	Mon Jul 11 13:36:08 2022 +0200
@@ -48,7 +48,7 @@
         (if (name == "") "" else " AND " + Data.name.equal(name))
   }
 
-  sealed case class Entry_Name(session: String, theory: String, name: String) {
+  sealed case class Entry_Name(session: String = "", theory: String = "", name: String = "") {
     def readable(db: SQL.Database): Boolean = {
       val select = Data.table.select(List(Data.name), Data.where_equal(session, theory, name))
       db.using_statement(select)(stmt => stmt.execute_query().next())
@@ -112,7 +112,8 @@
     if (a.isEmpty) b else a + ":" + b
 
   def empty_entry(theory_name: String, name: String): Entry =
-    Entry(Entry_Name("", theory_name, name), false, Future.value(false, Bytes.empty), XML.Cache.none)
+    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,
@@ -192,7 +193,7 @@
     val body =
       if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.xz))
       else Future.value((false, bytes))
-    val entry_name = Entry_Name(session_name, args.theory_name, args.name)
+    val entry_name = Entry_Name(session = session_name, theory = args.theory_name, name = args.name)
     Entry(entry_name, args.executable, body, cache)
   }
 
@@ -277,7 +278,8 @@
     ) : Provider = {
       new Provider {
         def apply(export_name: String): Option[Entry] =
-          Entry_Name(session_name, theory_name, export_name).read(db, cache)
+          Entry_Name(session = session_name, theory = theory_name, name = export_name)
+            .read(db, cache)
 
         def focus(other_theory: String): Provider =
           if (other_theory == theory_name) this
@@ -312,7 +314,8 @@
     ) : Provider = {
       new Provider {
         def apply(export_name: String): Option[Entry] =
-          Entry_Name(session_name, theory_name, export_name).read(dir, cache)
+          Entry_Name(session = session_name, theory = theory_name, name = export_name)
+            .read(dir, cache)
 
         def focus(other_theory: String): Provider =
           if (other_theory == theory_name) this
@@ -363,7 +366,8 @@
           val matcher = make_matcher(export_patterns)
           for {
             (theory_name, name) <- export_names if matcher(theory_name, name)
-            entry <- Entry_Name(session_name, theory_name, name).read(db, store.cache)
+            entry <- Entry_Name(session = session_name, theory = theory_name, name = name)
+              .read(db, store.cache)
           } {
             val elems = theory_name :: space_explode('/', name)
             val path =
diff -r ca8ae1ffd2b8 -r 88598f7c9614 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Jul 11 13:21:22 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Jul 11 13:36:08 2022 +0200
@@ -1216,12 +1216,15 @@
         database_server match {
           case Some(db) =>
             sessions.view.map(session_name =>
-              Export.Entry_Name(session_name, theory_name, name).read(db, store.cache))
+              Export.Entry_Name(session = session_name, theory = theory_name, name = name)
+                .read(db, store.cache))
           case None =>
             sessions.view.map(session_name =>
               store.try_open_database(session_name) match {
                 case Some(db) =>
-                  using(db)(Export.Entry_Name(session_name, theory_name, name).read(_, store.cache))
+                  using(db) { _ =>
+                    Export.Entry_Name(session = session_name, theory = theory_name, name = name)
+                      .read(db, store.cache) }
                 case None => None
               })
         }