# HG changeset patch # User wenzelm # Date 1607445024 -3600 # Node ID 6c660f05f70cc298a4cbeb258e33bccd5f5f8cb9 # Parent d0038b553e0e4ddad46dd733aa13af337b759f5b clarified signature; diff -r d0038b553e0e -r 6c660f05f70c src/Pure/Admin/build_doc.scala --- 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 diff -r d0038b553e0e -r 6c660f05f70c src/Pure/Thy/export.scala --- 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 diff -r d0038b553e0e -r 6c660f05f70c src/Pure/Thy/presentation.scala --- 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)) diff -r d0038b553e0e -r 6c660f05f70c src/Pure/Thy/sessions.scala --- 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] = { diff -r d0038b553e0e -r 6c660f05f70c src/Pure/Tools/build.scala --- 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 + " ...") diff -r d0038b553e0e -r 6c660f05f70c src/Pure/Tools/build_job.scala --- 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,