# HG changeset patch
# User wenzelm
# Date 1659727765 -7200
# Node ID 11b2bf6f90d81ca7ffb9d16a093aaead7aaa85a3
# Parent  9dbcc4c66e1c6b3bb7de3997d97558ee509b7a24
clarified signature: less redundant -- Sessions.Base_Info already specifies the main session;

diff -r 9dbcc4c66e1c -r 11b2bf6f90d8 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Aug 05 21:18:02 2022 +0200
+++ b/src/Pure/Thy/export.scala	Fri Aug 05 21:29:25 2022 +0200
@@ -347,12 +347,11 @@
 
   def open_session_context(
     store: Sessions.Store,
-    session: String,
-    resources: Resources,
+    session_base_info: Sessions.Base_Info,
     document_snapshot: Option[Document.Snapshot] = None
   ): Session_Context = {
-    open_context(store)
-      .open_session(session, resources, document_snapshot = document_snapshot, close_context = true)
+    open_context(store).open_session(
+      session_base_info, document_snapshot = document_snapshot, close_context = true)
   }
 
   class Session_Database private[Export](val session: String, val db: SQL.Database) {
@@ -370,13 +369,14 @@
     def close(): Unit = ()
 
     def open_session(
-      session: String,
-      resources: Resources,
+      session_base_info: Sessions.Base_Info,
       document_snapshot: Option[Document.Snapshot] = None,
       close_context: Boolean = false
     ): Session_Context = {
-      val session_hierarchy = resources.sessions_structure.build_hierarchy(session)
-      val session_databases: List[Session_Database] =
+      val session_base = session_base_info.check.base
+      val session_hierarchy =
+        session_base_info.sessions_structure.build_hierarchy(session_base.session_name)
+      val session_databases =
         db_context.database_server match {
           case Some(db) => session_hierarchy.map(name => new Session_Database(name, db))
           case None =>
@@ -392,7 +392,7 @@
                 }
             }
         }
-      new Session_Context(resources, db_context.cache, session_databases, document_snapshot) {
+      new Session_Context(db_context.cache, session_base, session_databases, document_snapshot) {
         override def close(): Unit = {
           session_databases.foreach(_.close())
           if (close_context) context.close()
@@ -402,8 +402,8 @@
   }
 
   class Session_Context private[Export](
-    val resources: Resources,
     val cache: Term.Cache,
+    session_base: Sessions.Base,
     db_hierarchy: List[Session_Database],
     document_snapshot: Option[Document.Snapshot]
   ) extends AutoCloseable {
@@ -413,7 +413,7 @@
 
     def session_name: String =
       if (document_snapshot.isDefined) Sessions.DRAFT
-      else resources.session_base.session_name
+      else session_base.session_name
 
     def session_stack: List[String] =
       ((if (document_snapshot.isDefined) List(session_name) else Nil) :::
diff -r 9dbcc4c66e1c -r 11b2bf6f90d8 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Aug 05 21:18:02 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Aug 05 21:29:25 2022 +0200
@@ -373,7 +373,6 @@
   ) {
     def check: Base_Info = if (errors.isEmpty) this else error(cat_lines(errors))
     def session: String = base.session_name
-    lazy val resources: Resources = new Resources(sessions_structure, check.base)
   }
 
   def base_info(options: Options,