src/Pure/Thy/export.scala

   }
 
 
   /* 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)
   }
 

         }
       }
     }
   }
 
+  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,
     db_hierarchy: List[Session_Database],
     document_snapshot: Option[Document.Snapshot]