--- a/src/Pure/Admin/build_doc.scala Sat Nov 21 20:35:48 2020 +0100
+++ b/src/Pure/Admin/build_doc.scala Sat Nov 21 21:02:38 2020 +0100
@@ -52,8 +52,10 @@
case (doc, session) =>
try {
progress.echo("Documentation " + doc + " ...")
- Presentation.build_documents(session, deps, store,
- output_pdf = Some(Path.explode("~~/src/doc")))
+
+ using(store.open_database_context(deps.sessions_structure))(db_context =>
+ Presentation.build_documents(session, deps, db_context,
+ output_pdf = Some(Path.explode("~~/src/doc"))))
None
}
catch {
--- a/src/Pure/Thy/export.scala Sat Nov 21 20:35:48 2020 +0100
+++ b/src/Pure/Thy/export.scala Sat Nov 21 21:02:38 2020 +0100
@@ -244,7 +244,7 @@
context: Sessions.Database_Context, session: String, theory_name: String): Provider =
new Provider {
def apply(export_name: String): Option[Entry] =
- context.try_export(session, theory_name, export_name)
+ context.read_export(session, theory_name, export_name)
def focus(other_theory: String): Provider = this
--- a/src/Pure/Thy/presentation.scala Sat Nov 21 20:35:48 2020 +0100
+++ b/src/Pure/Thy/presentation.scala Sat Nov 21 21:02:38 2020 +0100
@@ -14,6 +14,8 @@
{
/* document variants */
+ type Document_PDF = (Document_Variant, Bytes)
+
object Document_Variant
{
def parse(name: String, tags: String): Document_Variant =
@@ -79,8 +81,7 @@
}).toList)
}
- def read_document(db: SQL.Database, session_name: String, name: String)
- : Option[(Document_Variant, Bytes)] =
+ def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_PDF] =
{
val select = Data.table.select(sql = Data.where_equal(session_name, name))
db.using_statement(select)(stmt =>
@@ -234,14 +235,14 @@
def session_html(
session: String,
deps: Sessions.Deps,
- store: Sessions.Store,
- presentation: Context) =
+ db_context: Sessions.Database_Context,
+ presentation: Context)
{
val info = deps.sessions_structure(session)
val options = info.options
val base = deps(session)
- val session_dir = presentation.dir(store, info)
+ val session_dir = presentation.dir(db_context.store, info)
val session_fonts = Isabelle_System.make_directory(session_dir + Path.explode("fonts"))
for (entry <- Isabelle_Fonts.fonts(hidden = true))
File.copy(entry.path, session_fonts)
@@ -250,11 +251,10 @@
graphview.Graph_File.make_pdf(options, base.session_graph_display))
val documents =
- using(store.open_database(session))(db =>
- for {
- doc <- info.document_variants
- (_, pdf) <- Presentation.read_document(db, session, doc.name)
- } yield { Bytes.write(session_dir + doc.path.pdf, pdf); doc })
+ for {
+ doc <- info.document_variants
+ (_, pdf) <- db_context.read_document(session, doc.name)
+ } yield { Bytes.write(session_dir + doc.path.pdf, pdf); doc }
val links =
{
@@ -438,12 +438,12 @@
def build_documents(
session: String,
deps: Sessions.Deps,
- store: Sessions.Store,
+ db_context: Sessions.Database_Context,
progress: Progress = new Progress,
output_sources: Option[Path] = None,
output_pdf: Option[Path] = None,
verbose: Boolean = false,
- verbose_latex: Boolean = false): List[(Document_Variant, Bytes)] =
+ verbose_latex: Boolean = false): List[Document_PDF] =
{
/* session info */
@@ -456,13 +456,11 @@
/* prepare document directory */
lazy val tex_files =
- using(store.open_database_context(deps.sessions_structure))(context =>
- for (name <- base.session_theories ::: base.document_theories)
- yield {
- val entry = context.export(session, name.theory, document_tex_name(name))
- Path.basic(tex_name(name)) -> entry.uncompressed(cache = store.xz_cache)
- }
- )
+ for (name <- base.session_theories ::: base.document_theories)
+ yield {
+ val entry = db_context.get_export(session, name.theory, document_tex_name(name))
+ Path.basic(tex_name(name)) -> entry.uncompressed(cache = db_context.xz_cache)
+ }
def prepare_dir1(dir: Path, doc: Document_Variant): (Path, String) =
{
@@ -521,15 +519,14 @@
// old document from database
val old_document =
- using(store.open_database(session))(db =>
- for {
- document@(doc, pdf) <- read_document(db, session, doc.name)
- if doc.sources == sources
- }
- yield {
- Bytes.write(doc_dir + doc.path.pdf, pdf)
- document
- })
+ for {
+ document@(doc, pdf) <- db_context.read_document(session, doc.name)
+ if doc.sources == sources
+ }
+ yield {
+ Bytes.write(doc_dir + doc.path.pdf, pdf)
+ document
+ }
old_document getOrElse {
// bash scripts
@@ -661,9 +658,10 @@
progress.echo_warning("No output directory")
}
- build_documents(session, deps, store, progress = progress,
- output_sources = output_sources, output_pdf = output_pdf,
- verbose = true, verbose_latex = verbose_latex)
+ using(store.open_database_context(deps.sessions_structure))(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 Sat Nov 21 20:35:48 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Sat Nov 21 21:02:38 2020 +0100
@@ -1182,12 +1182,15 @@
class Database_Context private[Sessions](
val store: Sessions.Store,
- sessions_structure: Sessions.Structure,
+ val sessions_structure: Sessions.Structure,
database_server: Option[SQL.Database]) extends AutoCloseable
{
+ def xml_cache: XML.Cache = store.xml_cache
+ def xz_cache: XZ.Cache = store.xz_cache
+
def close { database_server.foreach(_.close) }
- def try_export(session: String, theory_name: String, name: String): Option[Export.Entry] =
+ def read_export(session: String, theory_name: String, name: String): Option[Export.Entry] =
{
val hierarchy = sessions_structure.build_graph.all_preds(List(session)).view
val attempts =
@@ -1204,10 +1207,20 @@
attempts.collectFirst({ case Some(entry) => entry })
}
- def export(session: String, theory_name: String, name: String): Export.Entry =
- try_export(session, theory_name, name) getOrElse
+ 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 read_document(session_name: String, name: String): Option[Presentation.Document_PDF] =
+ database_server match {
+ case Some(db) => Presentation.read_document(db, session_name, name)
+ case None =>
+ store.try_open_database(session_name) match {
+ case Some(db) => using(db)(Presentation.read_document(_, session_name, name))
+ case None => None
+ }
+ }
+
override def toString: String =
{
val s =
--- a/src/Pure/Tools/build.scala Sat Nov 21 20:35:48 2020 +0100
+++ b/src/Pure/Tools/build.scala Sat Nov 21 21:02:38 2020 +0100
@@ -502,11 +502,12 @@
val presentation_dir = presentation.dir(store)
progress.echo("Presentation in " + presentation_dir.absolute)
- for ((_, (session_name, _)) <- presentation_chapters) {
- progress.expose_interrupt()
- progress.echo("Presenting " + session_name + " ...")
- Presentation.session_html(session_name, deps, store, presentation)
- }
+ using(store.open_database_context(deps.sessions_structure))(db_context =>
+ for ((_, (session_name, _)) <- presentation_chapters) {
+ progress.expose_interrupt()
+ progress.echo("Presenting " + session_name + " ...")
+ Presentation.session_html(session_name, deps, db_context, presentation)
+ })
val browser_chapters =
presentation_chapters.groupBy(_._1).
--- a/src/Pure/Tools/build_job.scala Sat Nov 21 20:35:48 2020 +0100
+++ b/src/Pure/Tools/build_job.scala Sat Nov 21 21:02:38 2020 +0100
@@ -227,12 +227,13 @@
progress.echo_document(msg)
}
val documents =
- Presentation.build_documents(session_name, deps, store,
- output_sources = info.document_output,
- output_pdf = info.document_output,
- progress = document_progress,
- verbose = verbose,
- verbose_latex = true)
+ using(store.open_database_context(deps.sessions_structure))(db_context =>
+ Presentation.build_documents(session_name, deps, db_context,
+ output_sources = info.document_output,
+ output_pdf = info.document_output,
+ progress = document_progress,
+ verbose = verbose,
+ verbose_latex = true))
using(store.open_database(session_name, output = true))(db =>
for ((doc, pdf) <- documents) {
db.transaction {