--- a/src/Pure/Thy/export.scala Sat Aug 06 23:13:35 2022 +0200
+++ b/src/Pure/Thy/export.scala Sun Aug 07 12:22:43 2022 +0200
@@ -241,24 +241,7 @@
}
- /* context for retrieval */
-
- def context(db_context: Sessions.Database_Context): Context = new Context(db_context)
-
- def open_context(store: Sessions.Store): Context =
- new Context(store.open_database_context()) { override def close(): Unit = db_context.close() }
-
- def open_session_context0(store: Sessions.Store, session: String): Session_Context =
- open_context(store).open_session0(session, close_context = true)
-
- def open_session_context(
- store: Sessions.Store,
- session_base_info: Sessions.Base_Info,
- document_snapshot: Option[Document.Snapshot] = None
- ): Session_Context = {
- open_context(store).open_session(
- session_base_info, document_snapshot = document_snapshot, close_context = true)
- }
+ /* context for database access */
class Session_Database private[Export](val session: String, val db: SQL.Database) {
def close(): Unit = ()
@@ -267,31 +250,62 @@
lazy val entry_names: List[Entry_Name] = read_entry_names(db, session)
}
- class Context private[Export](protected val db_context: Sessions.Database_Context)
- extends AutoCloseable {
- context =>
+ 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)
+ }
+
+ def open_session_context0(store: Sessions.Store, session: String): Session_Context =
+ open_database_context(store).open_session0(session, close_database_context = true)
- override def toString: String = db_context.toString
+ def open_session_context(
+ store: Sessions.Store,
+ session_base_info: Sessions.Base_Info,
+ document_snapshot: Option[Document.Snapshot] = None
+ ): Session_Context = {
+ open_database_context(store).open_session(
+ session_base_info, document_snapshot = document_snapshot, close_database_context = true)
+ }
- def cache: Term.Cache = db_context.cache
+ class Database_Context private[Export](
+ val store: Sessions.Store,
+ val database_server: Option[SQL.Database]
+ ) extends AutoCloseable {
+ database_context =>
- def close(): Unit = ()
+ override def toString: String = {
+ val s =
+ database_server match {
+ case Some(db) => db.toString
+ case None => "input_dirs = " + store.input_dirs.map(_.absolute).mkString(", ")
+ }
+ "Database_Context(" + s + ")"
+ }
+
+ def cache: Term.Cache = store.cache
- def open_session0(session: String, close_context: Boolean = false): Session_Context =
- open_session(Sessions.base_info0(session), close_context = close_context)
+ def close(): Unit = database_server.foreach(_.close())
+
+ def database_output[A](session: String)(f: SQL.Database => A): A =
+ database_server match {
+ case Some(db) => f(db)
+ case None => using(store.open_database(session, output = true))(f)
+ }
+
+ def open_session0(session: String, close_database_context: Boolean = false): Session_Context =
+ open_session(Sessions.base_info0(session), close_database_context = close_database_context)
def open_session(
session_base_info: Sessions.Base_Info,
document_snapshot: Option[Document.Snapshot] = None,
- close_context: Boolean = false
+ close_database_context: Boolean = false
): Session_Context = {
val session_name = session_base_info.check.base.session_name
val session_hierarchy = session_base_info.sessions_structure.build_hierarchy(session_name)
val session_databases =
- db_context.database_server match {
+ database_server match {
case Some(db) => session_hierarchy.map(name => new Session_Database(name, db))
case None =>
- val store = db_context.store
val attempts =
session_hierarchy.map(name => name -> store.try_open_database(name, server = false))
attempts.collectFirst({ case (name, None) => name }) match {
@@ -304,17 +318,17 @@
}
}
}
- new Session_Context(context, session_base_info, session_databases, document_snapshot) {
+ new Session_Context(database_context, session_base_info, session_databases, document_snapshot) {
override def close(): Unit = {
session_databases.foreach(_.close())
- if (close_context) context.close()
+ if (close_database_context) database_context.close()
}
}
}
}
class Session_Context private[Export](
- val export_context: Context,
+ val database_context: Database_Context,
session_base_info: Sessions.Base_Info,
db_hierarchy: List[Session_Database],
document_snapshot: Option[Document.Snapshot]
@@ -323,7 +337,7 @@
def close(): Unit = ()
- def cache: Term.Cache = export_context.cache
+ def cache: Term.Cache = database_context.cache
def sessions_structure: Sessions.Structure = session_base_info.sessions_structure
--- a/src/Pure/Thy/presentation.scala Sat Aug 06 23:13:35 2022 +0200
+++ b/src/Pure/Thy/presentation.scala Sun Aug 07 12:22:43 2022 +0200
@@ -113,13 +113,13 @@
val empty: Nodes = new Nodes(Map.empty, Map.empty)
def read(
- export_context: Export.Context,
+ database_context: Export.Database_Context,
deps: Sessions.Deps,
presentation_sessions: List[String]
): Nodes = {
def open_session(session: String): Export.Session_Context =
- export_context.open_session(deps.base_info(session))
+ database_context.open_session(deps.base_info(session))
type Batch = (String, List[String])
val batches =
--- a/src/Pure/Thy/sessions.scala Sat Aug 06 23:13:35 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Sun Aug 07 12:22:43 2022 +0200
@@ -1207,30 +1207,6 @@
val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
}
- class Database_Context private[Sessions](
- val store: Sessions.Store,
- val database_server: Option[SQL.Database]
- ) extends AutoCloseable {
- def cache: Term.Cache = store.cache
-
- def close(): Unit = database_server.foreach(_.close())
-
- def database_output[A](session: String)(f: SQL.Database => A): A =
- database_server match {
- case Some(db) => f(db)
- case None => using(store.open_database(session, output = true))(f)
- }
-
- override def toString: String = {
- val s =
- database_server match {
- case Some(db) => db.toString
- case None => "input_dirs = " + store.input_dirs.map(_.absolute).mkString(", ")
- }
- "Database_Context(" + s + ")"
- }
- }
-
def store(options: Options, cache: Term.Cache = Term.Cache.make()): Store =
new Store(options, cache)
@@ -1310,9 +1286,6 @@
port = options.int("build_database_ssh_port"))),
ssh_close = true)
- def open_database_context(server: Boolean = database_server): Database_Context =
- new Database_Context(store, if (server) Some(open_database_server()) else None)
-
def try_open_database(
name: String,
output: Boolean = false,
--- a/src/Pure/Tools/build.scala Sat Aug 06 23:13:35 2022 +0200
+++ b/src/Pure/Tools/build.scala Sun Aug 07 12:22:43 2022 +0200
@@ -494,9 +494,9 @@
Presentation.update_chapter(presentation_dir, chapter, entries)
}
- using(Export.open_context(store)) { export_context =>
+ using(Export.open_database_context(store)) { database_context =>
val presentation_nodes =
- Presentation.Nodes.read(export_context, deps, presentation_sessions.map(_.name))
+ Presentation.Nodes.read(database_context, deps, presentation_sessions.map(_.name))
Par_List.map({ (session: String) =>
progress.expose_interrupt()
@@ -510,7 +510,7 @@
deps.sessions_structure(deps(session).theory_qualifier(name))
}
- using(export_context.open_session(deps.base_info(session))) { session_context =>
+ using(database_context.open_session(deps.base_info(session))) { session_context =>
Presentation.session_html(session_context, deps,
progress = progress,
verbose = verbose,
--- a/src/Pure/Tools/build_job.scala Sat Aug 06 23:13:35 2022 +0200
+++ b/src/Pure/Tools/build_job.scala Sun Aug 07 12:22:43 2022 +0200
@@ -441,16 +441,16 @@
val (document_output, document_errors) =
try {
if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) {
- using(store.open_database_context()) { db_context =>
+ using(Export.open_database_context(store)) { database_context =>
val documents =
- using(Export.context(db_context).open_session(deps.base_info(session_name))) {
+ using(database_context.open_session(deps.base_info(session_name))) {
session_context =>
Document_Build.build_documents(
Document_Build.context(session_context, progress = progress),
output_sources = info.document_output,
output_pdf = info.document_output)
}
- db_context.database_output(session_name)(db =>
+ database_context.database_output(session_name)(db =>
documents.foreach(_.write(db, session_name)))
(documents.flatMap(_.log_lines), Nil)
}