clarified signature: less redundant -- Sessions.Base_Info already specifies the main session;
--- 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) :::
--- 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,