--- a/src/Pure/Admin/build_doc.scala Tue Dec 08 16:30:17 2020 +0100
+++ b/src/Pure/Admin/build_doc.scala Tue Dec 08 17:30:24 2020 +0100
@@ -53,7 +53,7 @@
try {
progress.echo("Documentation " + doc + " ...")
- using(store.open_database_context(deps.sessions_structure))(db_context =>
+ using(store.open_database_context())(db_context =>
Presentation.build_documents(session, deps, db_context,
output_pdf = Some(Path.explode("~~/doc"))))
None
--- a/src/Pure/Thy/export.scala Tue Dec 08 16:30:17 2020 +0100
+++ b/src/Pure/Thy/export.scala Tue Dec 08 17:30:24 2020 +0100
@@ -84,9 +84,8 @@
def compound_name(a: String, b: String): String = a + ":" + b
- def empty_entry(session_name: String, theory_name: String, name: String): Entry =
- Entry(session_name, theory_name, name, false,
- Future.value(false, Bytes.empty), XZ.no_cache())
+ def empty_entry(theory_name: String, name: String): Entry =
+ Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XZ.no_cache())
sealed case class Entry(
session_name: String,
@@ -260,10 +259,12 @@
}
def database_context(
- context: Sessions.Database_Context, session: String, theory_name: String): Provider =
+ context: Sessions.Database_Context,
+ sessions: List[String],
+ theory_name: String): Provider =
new Provider {
def apply(export_name: String): Option[Entry] =
- context.read_export(session, theory_name, export_name)
+ context.read_export(sessions, theory_name, export_name)
def focus(other_theory: String): Provider = this
--- a/src/Pure/Thy/presentation.scala Tue Dec 08 16:30:17 2020 +0100
+++ b/src/Pure/Thy/presentation.scala Tue Dec 08 17:30:24 2020 +0100
@@ -461,6 +461,7 @@
/* session info */
val info = deps.sessions_structure(session)
+ val hierarchy = deps.sessions_structure.hierarchy(session)
val options = info.options
val base = deps(session)
val graph_pdf = graphview.Graph_File.make_pdf(options, base.session_graph_display)
@@ -471,7 +472,7 @@
lazy val tex_files =
for (name <- base.session_theories ::: base.document_theories)
yield {
- val entry = db_context.get_export(session, name.theory, document_tex_name(name))
+ val entry = db_context.get_export(hierarchy, name.theory, document_tex_name(name))
Path.basic(tex_name(name)) -> entry.uncompressed
}
@@ -673,7 +674,7 @@
progress.echo_warning("No output directory")
}
- using(store.open_database_context(deps.sessions_structure))(db_context =>
+ using(store.open_database_context())(db_context =>
build_documents(session, deps, db_context, progress = progress,
output_sources = output_sources, output_pdf = output_pdf,
verbose = true, verbose_latex = verbose_latex))
--- a/src/Pure/Thy/sessions.scala Tue Dec 08 16:30:17 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Tue Dec 08 17:30:24 2020 +0100
@@ -821,6 +821,8 @@
deps
}
+ def hierarchy(session: String): List[String] = build_graph.all_preds(List(session))
+
def build_selection(sel: Selection): List[String] = selected(build_graph, sel)
def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
def build_requirements(ss: List[String]): List[String] = build_graph.all_preds_rev(ss)
@@ -1194,7 +1196,6 @@
class Database_Context private[Sessions](
val store: Sessions.Store,
- val sessions_structure: Sessions.Structure,
database_server: Option[SQL.Database]) extends AutoCloseable
{
def xml_cache: XML.Cache = store.xml_cache
@@ -1218,16 +1219,16 @@
}
}
- def read_export(session: String, theory_name: String, name: String): Option[Export.Entry] =
+ def read_export(
+ sessions: List[String], theory_name: String, name: String): Option[Export.Entry] =
{
- val hierarchy = sessions_structure.build_graph.all_preds(List(session)).view
val attempts =
database_server match {
case Some(db) =>
- hierarchy.map(session_name =>
+ sessions.view.map(session_name =>
Export.read_entry(db, store.xz_cache, session_name, theory_name, name))
case None =>
- hierarchy.map(session_name =>
+ sessions.view.map(session_name =>
store.try_open_database(session_name) match {
case Some(db) =>
using(db)(Export.read_entry(_, store.xz_cache, session_name, theory_name, name))
@@ -1237,9 +1238,10 @@
attempts.collectFirst({ case Some(entry) => entry })
}
- def get_export(session: String, theory_name: String, name: String): Export.Entry =
- read_export(session, theory_name, name) getOrElse
- Export.empty_entry(session, theory_name, name)
+ def get_export(
+ session_hierarchy: List[String], theory_name: String, name: String): Export.Entry =
+ read_export(session_hierarchy, theory_name, name) getOrElse
+ Export.empty_entry(theory_name, name)
override def toString: String =
{
@@ -1331,9 +1333,8 @@
port = options.int("build_database_ssh_port"))),
ssh_close = true)
- def open_database_context(sessions_structure: Sessions.Structure): Database_Context =
- new Database_Context(store, sessions_structure,
- if (database_server) Some(open_database_server()) else None)
+ def open_database_context(): Database_Context =
+ new Database_Context(store, if (database_server) Some(open_database_server()) else None)
def try_open_database(name: String, output: Boolean = false): Option[SQL.Database] =
{
--- a/src/Pure/Tools/build.scala Tue Dec 08 16:30:17 2020 +0100
+++ b/src/Pure/Tools/build.scala Tue Dec 08 17:30:24 2020 +0100
@@ -502,7 +502,7 @@
val presentation_dir = presentation.dir(store)
progress.echo("Presentation in " + presentation_dir.absolute)
- using(store.open_database_context(deps.sessions_structure))(db_context =>
+ using(store.open_database_context())(db_context =>
for ((_, (session_name, _)) <- presentation_chapters) {
progress.expose_interrupt()
progress.echo("Presenting " + session_name + " ...")
--- a/src/Pure/Tools/build_job.scala Tue Dec 08 16:30:17 2020 +0100
+++ b/src/Pure/Tools/build_job.scala Tue Dec 08 17:30:24 2020 +0100
@@ -12,11 +12,13 @@
object Build_Job
{
+ /* theory markup/messages from database */
+
def read_theory(
db_context: Sessions.Database_Context, session: String, theory: String): Option[Command] =
{
def read(name: String): Export.Entry =
- db_context.get_export(session, theory, name)
+ db_context.get_export(List(session), theory, name)
def read_xml(name: String): XML.Body =
db_context.xml_cache.body(
@@ -322,7 +324,7 @@
try {
if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty)
{
- using(store.open_database_context(deps.sessions_structure))(db_context =>
+ using(store.open_database_context())(db_context =>
{
val documents =
Presentation.build_documents(session_name, deps, db_context,