# HG changeset patch
# User wenzelm
# Date 1605988958 -3600
# Node ID b5e6f0d137a7849966a678a6c2e7c5b812239eba
# Parent  e0443773ef1a4bab60459243710d6468eaa053b8
clarified signature: prefer Database_Context;

diff -r e0443773ef1a -r b5e6f0d137a7 src/Pure/Admin/build_doc.scala
--- 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 {
diff -r e0443773ef1a -r b5e6f0d137a7 src/Pure/Thy/export.scala
--- 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
 
diff -r e0443773ef1a -r b5e6f0d137a7 src/Pure/Thy/presentation.scala
--- 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))
       }
     })
 }
diff -r e0443773ef1a -r b5e6f0d137a7 src/Pure/Thy/sessions.scala
--- 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 =
diff -r e0443773ef1a -r b5e6f0d137a7 src/Pure/Tools/build.scala
--- 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).
diff -r e0443773ef1a -r b5e6f0d137a7 src/Pure/Tools/build_job.scala
--- 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 {