# HG changeset patch # User wenzelm # Date 1659807118 -7200 # Node ID dba571dd0ba965d8a0992ac9d60d932279c6617b # Parent 0e5339342998edb42dfbf2e8a8f0a2e00b34e640 clarified signature: prefer Export.Session_Context over Sessions.Database_Context; discontinued obsolete operations; diff -r 0e5339342998 -r dba571dd0ba9 src/Pure/Admin/build_doc.scala --- a/src/Pure/Admin/build_doc.scala Sat Aug 06 17:28:59 2022 +0200 +++ b/src/Pure/Admin/build_doc.scala Sat Aug 06 19:31:58 2022 +0200 @@ -54,9 +54,11 @@ progress.expose_interrupt() progress.echo("Documentation " + quote(doc) + " ...") - using(store.open_database_context()) { db_context => - Document_Build.build_documents(Document_Build.context(session, deps, db_context), - output_pdf = Some(Path.explode("~~/doc"))) + using(Export.open_session_context(store, deps.base_info(session))) { + session_context => + Document_Build.build_documents( + Document_Build.context(session_context), + output_pdf = Some(Path.explode("~~/doc"))) } None } diff -r 0e5339342998 -r dba571dd0ba9 src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala Sat Aug 06 17:28:59 2022 +0200 +++ b/src/Pure/Thy/document_build.scala Sat Aug 06 19:31:58 2022 +0200 @@ -116,30 +116,23 @@ map(name => texinputs + Path.basic(name)) def context( - session: String, - deps: Sessions.Deps, - db_context: Sessions.Database_Context, + session_context: Export.Session_Context, progress: Progress = new Progress - ): Context = { - val structure = deps.sessions_structure - val info = structure(session) - val base = deps(session) - val hierarchy = deps.sessions_structure.build_hierarchy(session) - val classpath = db_context.get_classpath(structure, session) - new Context(info, base, hierarchy, db_context, classpath, progress) - } + ): Context = new Context(session_context, progress) final class Context private[Document_Build]( - info: Sessions.Info, - base: Sessions.Base, - hierarchy: List[String], - db_context: Sessions.Database_Context, - val classpath: List[File.Content_Bytes], + val session_context: Export.Session_Context, val progress: Progress = new Progress ) { /* session info */ - def session: String = info.name + def session: String = session_context.session_name + + private val info = session_context.sessions_structure(session) + private val base = session_context.session_base + + val classpath: List[File.Content_Bytes] = session_context.classpath() + def options: Options = info.options def document_bibliography: Boolean = options.bool("document_bibliography") @@ -159,9 +152,6 @@ .find(_.name == name).getOrElse(error("Bad document_build engine " + quote(name))) } - def get_export(theory: String, name: String): Export.Entry = - db_context.get_export(hierarchy, theory, name) - /* document content */ @@ -176,7 +166,8 @@ for (name <- document_theories) yield { val path = Path.basic(tex_name(name)) - val content = YXML.parse_body(get_export(name.theory, Export.DOCUMENT_LATEX).text) + val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true) + val content = YXML.parse_body(entry.text) File.Content(path, content) } @@ -255,7 +246,8 @@ def old_document(directory: Directory): Option[Document_Output] = for { - old_doc <- db_context.database(session)(read_document(_, session, directory.doc.name)) + db <- session_context.session_db() + old_doc <- read_document(db, session, directory.doc.name) if old_doc.sources == directory.sources } yield old_doc @@ -481,12 +473,15 @@ Sessions.load_structure(options + "document=pdf", dirs = dirs). selection_deps(Sessions.Selection.session(session)) + val session_base_info = deps.base_info(session) + if (output_sources.isEmpty && output_pdf.isEmpty) { progress.echo_warning("No output directory") } - using(store.open_database_context()) { db_context => - build_documents(context(session, deps, db_context, progress = progress), + using(Export.open_session_context(store, session_base_info)) { session_context => + build_documents( + context(session_context, progress = progress), output_sources = output_sources, output_pdf = output_pdf, verbose = verbose_latex) } diff -r 0e5339342998 -r dba571dd0ba9 src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Sat Aug 06 17:28:59 2022 +0200 +++ b/src/Pure/Thy/export.scala Sat Aug 06 19:31:58 2022 +0200 @@ -267,11 +267,14 @@ lazy val entry_names: List[Entry_Name] = read_entry_names(db, session) } - class Context private[Export](val db_context: Sessions.Database_Context) extends AutoCloseable { + class Context private[Export](protected val db_context: Sessions.Database_Context) + extends AutoCloseable { context => override def toString: String = db_context.toString + def cache: Term.Cache = db_context.cache + def close(): Unit = () def open_session0(session: String, close_context: Boolean = false): Session_Context = @@ -320,9 +323,7 @@ def close(): Unit = () - def db_context: Sessions.Database_Context = export_context.db_context - - def cache: Term.Cache = export_context.db_context.cache + def cache: Term.Cache = export_context.cache def sessions_structure: Sessions.Structure = session_base_info.sessions_structure @@ -392,7 +393,19 @@ def theory(theory: String): Theory_Context = new Theory_Context(session_context, theory) - override def toString: String = + def classpath(): List[File.Content_Bytes] = { + (for { + session <- session_stack.iterator + info <- sessions_structure.get(session).iterator + if info.export_classpath.nonEmpty + matcher = make_matcher(info.export_classpath) + entry_name <- entry_names(session = session).iterator + if matcher(entry_name) + entry <- get(entry_name.theory, entry_name.name).iterator + } yield File.Content(entry.entry_name.make_path(), entry.uncompressed)).toList + } + + override def toString: String = "Export.Session_Context(" + commas_quote(session_stack) + ")" } diff -r 0e5339342998 -r dba571dd0ba9 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sat Aug 06 17:28:59 2022 +0200 +++ b/src/Pure/Thy/sessions.scala Sat Aug 06 19:31:58 2022 +0200 @@ -1221,56 +1221,6 @@ case None => using(store.open_database(session, output = true))(f) } - def database[A](session: String)(f: SQL.Database => Option[A]): Option[A] = - database_server match { - case Some(db) => f(db) - case None => - store.try_open_database(session) match { - case Some(db) => using(db)(f) - case None => None - } - } - - def read_export( - session_hierarchy: List[String], theory: String, name: String - ): Option[Export.Entry] = { - def read(db: SQL.Database, session: String): Option[Export.Entry] = - Export.Entry_Name(session = session, theory = theory, name = name).read(db, store.cache) - val attempts = - database_server match { - case Some(db) => session_hierarchy.view.map(read(db, _)) - case None => - session_hierarchy.view.map(session => - store.try_open_database(session) match { - case Some(db) => using(db) { _ => read(db, session) } - case None => None - }) - } - attempts.collectFirst({ case Some(entry) => entry }) - } - - def get_export(session_hierarchy: List[String], theory: String, name: String): Export.Entry = - read_export(session_hierarchy, theory, name) getOrElse - Export.empty_entry(theory, name) - - def get_classpath(structure: Structure, session: String): List[File.Content_Bytes] = - { - (for { - name <- structure.build_requirements(List(session)) - patterns = structure(name).export_classpath if patterns.nonEmpty - } yield { - database(name) { db => - val matcher = Export.make_matcher(patterns) - val res = - for { - entry_name <- Export.read_entry_names(db, name) if matcher(entry_name) - entry <- entry_name.read(db, store.cache) - } yield File.Content(entry.entry_name.make_path(), entry.uncompressed) - Some(res) - }.getOrElse(Nil) - }).flatten - } - override def toString: String = { val s = database_server match { diff -r 0e5339342998 -r dba571dd0ba9 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Sat Aug 06 17:28:59 2022 +0200 +++ b/src/Pure/Tools/build_job.scala Sat Aug 06 19:31:58 2022 +0200 @@ -443,10 +443,13 @@ if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) { using(store.open_database_context()) { db_context => val documents = - Document_Build.build_documents( - Document_Build.context(session_name, deps, db_context, progress = progress), - output_sources = info.document_output, - output_pdf = info.document_output) + using(Export.context(db_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 => documents.foreach(_.write(db, session_name))) (documents.flatMap(_.log_lines), Nil)