--- a/src/Pure/Thy/document_build.scala Tue Aug 02 16:02:06 2022 +0200
+++ b/src/Pure/Thy/document_build.scala Tue Aug 02 19:25:37 2022 +0200
@@ -253,7 +253,7 @@
def old_document(directory: Directory): Option[Document_Output] =
for {
- old_doc <- db_context.input_database(session)(read_document(_, session, directory.doc.name))
+ old_doc <- db_context.database(session)(read_document(_, session, directory.doc.name))
if old_doc.sources == directory.sources
}
yield old_doc
--- a/src/Pure/Thy/presentation.scala Tue Aug 02 16:02:06 2022 +0200
+++ b/src/Pure/Thy/presentation.scala Tue Aug 02 19:25:37 2022 +0200
@@ -125,7 +125,7 @@
val theory_node_info =
Par_List.map[Batch, List[(String, Node_Info)]](
{ case (session, thys) =>
- db_context.input_database(session) { db =>
+ db_context.database(session) { db =>
val provider0 = Export.Provider.database(db, db_context.cache, session, "")
val result =
for (thy_name <- thys) yield {
@@ -530,7 +530,7 @@
val documents =
for {
doc <- info.document_variants
- document <- db_context.input_database(session)(db =>
+ document <- db_context.database(session)(db =>
Document_Build.read_document(db, session, doc.name))
} yield {
val doc_path = (session_dir + doc.path.pdf).expand
--- a/src/Pure/Thy/sessions.scala Tue Aug 02 16:02:06 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Tue Aug 02 19:25:37 2022 +0200
@@ -1200,13 +1200,13 @@
def close(): Unit = database_server.foreach(_.close())
- def output_database[A](session: String)(f: SQL.Database => A): A =
+ 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 input_database[A](session: String)(f: SQL.Database => Option[A]): Option[A] =
+ def database[A](session: String)(f: SQL.Database => Option[A]): Option[A] =
database_server match {
case Some(db) => f(db)
case None =>
@@ -1244,7 +1244,7 @@
name <- structure.build_requirements(List(session))
patterns = structure(name).export_classpath if patterns.nonEmpty
} yield {
- input_database(name) { db =>
+ database(name) { db =>
db.transaction {
val matcher = Export.make_matcher(patterns)
val res =
--- a/src/Pure/Tools/build_job.scala Tue Aug 02 16:02:06 2022 +0200
+++ b/src/Pure/Tools/build_job.scala Tue Aug 02 19:25:37 2022 +0200
@@ -94,7 +94,7 @@
using(store.open_database_context()) { db_context =>
val result =
- db_context.input_database(session_name) { db =>
+ db_context.database(session_name) { db =>
val theories = store.read_theories(db, session_name)
val errors = store.read_errors(db, session_name)
store.read_build(db, session_name).map(info => (theories, errors, info.return_code))
@@ -448,7 +448,7 @@
Document_Build.context(session_name, deps, db_context, progress = progress),
output_sources = info.document_output,
output_pdf = info.document_output)
- db_context.output_database(session_name)(db =>
+ db_context.database_output(session_name)(db =>
documents.foreach(_.write(db, session_name)))
(documents.flatMap(_.log_lines), Nil)
}
--- a/src/Pure/Tools/profiling_report.scala Tue Aug 02 16:02:06 2022 +0200
+++ b/src/Pure/Tools/profiling_report.scala Tue Aug 02 19:25:37 2022 +0200
@@ -18,8 +18,7 @@
val store = Sessions.store(options)
using(store.open_database_context()) { db_context =>
- val result =
- db_context.input_database(session)(db => Some(store.read_theories(db, session)))
+ val result = db_context.database(session)(db => Some(store.read_theories(db, session)))
result match {
case None => error("Missing build database for session " + quote(session))
case Some(used_theories) =>