# HG changeset patch
# User wenzelm
# Date 1659868677 -7200
# Node ID 4827096caeb5b17dd84c7a5be39f517cb5c698ce
# Parent  0132026e26eb0f57d0658283760092b27b45c112
tuned;

diff -r 0132026e26eb -r 4827096caeb5 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sun Aug 07 12:37:15 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sun Aug 07 12:37:57 2022 +0200
@@ -243,14 +243,6 @@
 
   /* context for database access */
 
-  class Session_Database private[Export](val session: String, val db: SQL.Database)
-  extends AutoCloseable {
-    def close(): Unit = ()
-
-    lazy private [Export] val theory_names: List[String] = read_theory_names(db, session)
-    lazy private [Export] val entry_names: List[Entry_Name] = read_entry_names(db, session)
-  }
-
   def open_database_context(store: Sessions.Store): Database_Context = {
     val database_server = if (store.database_server) Some(store.open_database_server()) else None
     new Database_Context(store, database_server)
@@ -331,6 +323,14 @@
     }
   }
 
+  class Session_Database private[Export](val session: String, val db: SQL.Database)
+  extends AutoCloseable {
+    def close(): Unit = ()
+
+    lazy private [Export] val theory_names: List[String] = read_theory_names(db, session)
+    lazy private [Export] val entry_names: List[Entry_Name] = read_entry_names(db, session)
+  }
+
   class Session_Context private[Export](
     val database_context: Database_Context,
     session_base_info: Sessions.Base_Info,