clarified access to single database server vs. collection of database files;

--- a/src/Pure/Thy/export.scala	Mon Nov 16 23:49:20 2020 +0100
+++ b/src/Pure/Thy/export.scala	Tue Nov 17 16:34:01 2020 +0100
@@ -75,6 +75,9 @@
 
   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))
+
   sealed case class Entry(
     session_name: String,
     theory_name: String,
@@ -182,6 +185,55 @@
   }
 
 
+  /* database context */
+
+  def open_database_context(
+    sessions_structure: Sessions.Structure,
+    store: Sessions.Store): Database_Context =
+  {
+    new Database_Context(sessions_structure, store,
+      if (store.database_server) Some(store.open_database_server()) else None)
+  }
+
+  class Database_Context private[Export](
+    sessions_structure: Sessions.Structure,
+    store: Sessions.Store,
+    database_server: Option[SQL.Database]) extends AutoCloseable
+  {
+    def close { database_server.foreach(_.close) }
+
+    def try_entry(session: String, theory_name: String, name: String): Option[Entry] =
+    {
+      val hierarchy = sessions_structure.build_graph.all_preds(List(session)).view
+      val attempts =
+        database_server match {
+          case Some(db) =>
+            hierarchy.map(session_name => read_entry(db, session_name, theory_name, name))
+          case None =>
+            hierarchy.map(session_name =>
+              store.try_open_database(session_name) match {
+                case Some(db) => using(db)(read_entry(_, session_name, theory_name, name))
+                case None => None
+              })
+        }
+      attempts.collectFirst({ case Some(entry) => entry })
+    }
+
+    def entry(session: String, theory_name: String, name: String): Entry =
+      try_entry(session, theory_name, name) getOrElse empty_entry(session, theory_name, name)
+
+    override def toString: String =
+    {
+      val s =
+        database_server match {
+          case Some(db) => db.toString
+          case None => "input_dirs = " + store.input_dirs.map(_.absolute).mkString(", ")
+        }
+      "Database_Context(" + s + ")"
+    }
+  }
+
+
   /* database consumer thread */
 
   def consumer(db: SQL.Database, cache: XZ.Cache = XZ.cache()): Consumer = new Consumer(db, cache)
@@ -237,6 +289,17 @@
         override def toString: String = "none"
       }
 
+    def database_context(
+        context: Database_Context, session: String, theory_name: String): Provider =
+      new Provider {
+        def apply(export_name: String): Option[Entry] =
+          context.try_entry(session, theory_name, export_name)
+
+        def focus(other_theory: String): Provider = this
+
+        override def toString: String = context.toString
+      }
+
     def database(db: SQL.Database, session_name: String, theory_name: String): Provider =
       new Provider {
         def apply(export_name: String): Option[Entry] =

--- a/src/Pure/Thy/present.scala	Mon Nov 16 23:49:20 2020 +0100
+++ b/src/Pure/Thy/present.scala	Tue Nov 17 16:34:01 2020 +0100
@@ -119,10 +119,10 @@
     }
 
     val theories =
-      using(store.open_database(session))(db =>
+      using(Export.open_database_context(deps.sessions_structure, store))(context =>
         for {
           name <- base.session_theories
-          entry <- Export.read_entry(db, session, name.theory, document_html_name(name))
+          entry <- context.try_entry(session, name.theory, document_html_name(name))
         } yield name -> entry.uncompressed(cache = store.xz_cache))
 
     val theories_body =
@@ -265,20 +265,17 @@
     val base = deps(session)
     val graph_pdf = graphview.Graph_File.make_pdf(options, base.session_graph_display)
 
-    def find_tex(name: Document.Node.Name): Option[Bytes] =
-      deps.sessions_structure.build_requirements(List(session)).reverse.view
-        .map(session_name =>
-          using(store.open_database(session_name))(db =>
-            Export.read_entry(db, session_name, name.theory, document_tex_name(name)).
-              map(_.uncompressed(cache = store.xz_cache))))
-        .collectFirst({ case Some(x) => x })
-
 
     /* prepare document directory */
 
     lazy val tex_files =
-      for (name <- base.session_theories ::: base.document_theories)
-        yield Path.basic(tex_name(name)) -> find_tex(name).getOrElse(Bytes.empty)
+      using(Export.open_database_context(deps.sessions_structure, store))(context =>
+        for (name <- base.session_theories ::: base.document_theories)
+        yield {
+          val entry = context.entry(session, name.theory, document_tex_name(name))
+          Path.basic(tex_name(name)) -> entry.uncompressed(cache = store.xz_cache)
+        }
+      )
 
     def prepare_dir(dir: Path, doc_name: String, doc_tags: List[String]): (Path, String) =
     {

--- a/src/Pure/Thy/sessions.scala	Mon Nov 16 23:49:20 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Nov 17 16:34:01 2020 +0100
@@ -1171,7 +1171,9 @@
 
   class Store private[Sessions](val options: Options)
   {
-    override def toString: String = "Store(output_dir = " + output_dir.expand + ")"
+    store =>
+
+    override def toString: String = "Store(output_dir = " + output_dir.absolute + ")"
 
     val xml_cache: XML.Cache = XML.make_cache()
     val xz_cache: XZ.Cache = XZ.make_cache()
@@ -1227,33 +1229,41 @@
 
     /* database */
 
-    private def database_server: Boolean = options.bool("build_database_server")
+    def database_server: Boolean = options.bool("build_database_server")
 
-    def access_database(name: String, output: Boolean = false): Option[SQL.Database] =
+    def open_database_server(): SQL.Database =
+      PostgreSQL.open_database(
+        user = options.string("build_database_user"),
+        password = options.string("build_database_password"),
+        database = options.string("build_database_name"),
+        host = options.string("build_database_host"),
+        port = options.int("build_database_port"),
+        ssh =
+          options.proper_string("build_database_ssh_host").map(ssh_host =>
+            SSH.open_session(options,
+              host = ssh_host,
+              user = options.string("build_database_ssh_user"),
+              port = options.int("build_database_ssh_port"))),
+        ssh_close = true)
+
+    def try_open_database(name: String, output: Boolean = false): Option[SQL.Database] =
     {
-      if (database_server) {
-        val db =
-          PostgreSQL.open_database(
-            user = options.string("build_database_user"),
-            password = options.string("build_database_password"),
-            database = options.string("build_database_name"),
-            host = options.string("build_database_host"),
-            port = options.int("build_database_port"),
-            ssh =
-              options.proper_string("build_database_ssh_host").map(ssh_host =>
-                SSH.open_session(options,
-                  host = ssh_host,
-                  user = options.string("build_database_ssh_user"),
-                  port = options.int("build_database_ssh_port"))),
-            ssh_close = true)
-        if (output || has_session_info(db, name)) Some(db) else { db.close; None }
+      def check(db: SQL.Database): Option[SQL.Database] =
+        if (output || session_info_exists(db)) Some(db) else { db.close; None }
+
+      if (database_server) check(open_database_server())
+      else if (output) Some(SQLite.open_database(output_database(name)))
+      else {
+        (for {
+          dir <- input_dirs.view
+          path = dir + database(name) if path.is_file
+          db <- check(SQLite.open_database(path))
+        } yield db).headOption
       }
-      else if (output) Some(SQLite.open_database(output_database(name)))
-      else input_dirs.map(_ + database(name)).find(_.is_file).map(SQLite.open_database)
     }
 
     def open_database(name: String, output: Boolean = false): SQL.Database =
-      access_database(name, output = output) getOrElse
+      try_open_database(name, output = output) getOrElse
         error("Missing build database for session " + quote(name))
 
     def clean_output(name: String): (Boolean, Boolean) =
@@ -1261,11 +1271,11 @@
       val relevant_db =
         database_server &&
         {
-          access_database(name) match {
+          try_open_database(name) match {
             case Some(db) =>
               try {
                 db.transaction {
-                  val relevant_db = has_session_info(db, name)
+                  val relevant_db = session_info_defined(db, name)
                   init_session_info(db, name)
                   relevant_db
                 }
@@ -1318,17 +1328,22 @@
       }
     }
 
-    def has_session_info(db: SQL.Database, name: String): Boolean =
+    def session_info_exists(db: SQL.Database): Boolean =
     {
+      val tables = db.tables
+      tables.contains(Session_Info.table.name) &&
+      tables.contains(Export.Data.table.name)
+    }
+
+    def session_info_defined(db: SQL.Database, name: String): Boolean =
       db.transaction {
-        db.tables.contains(Session_Info.table.name) &&
+        session_info_exists(db) &&
         {
           db.using_statement(
             Session_Info.table.select(List(Session_Info.session_name),
               Session_Info.session_name.where_equal(name)))(stmt => stmt.execute_query().next())
         }
       }
-    }
 
     def write_session_info(
       db: SQL.Database,

--- a/src/Pure/Tools/build.scala	Mon Nov 16 23:49:20 2020 +0100
+++ b/src/Pure/Tools/build.scala	Tue Nov 17 16:34:01 2020 +0100
@@ -38,7 +38,7 @@
     {
       val no_timings: Timings = (Nil, 0.0)
 
-      store.access_database(session_name) match {
+      store.try_open_database(session_name) match {
         case None => no_timings
         case Some(db) =>
           def ignore_error(msg: String) =
@@ -545,7 +545,7 @@
       if (soft_build && !fresh_build) {
         val outdated =
           deps0.sessions_structure.build_topological_order.flatMap(name =>
-            store.access_database(name) match {
+            store.try_open_database(name) match {
               case Some(db) =>
                 using(db)(store.read_build(_, name)) match {
                   case Some(build)
@@ -702,7 +702,7 @@
 
                 val (current, heap_digest) =
                 {
-                  store.access_database(session_name) match {
+                  store.try_open_database(session_name) match {
                     case Some(db) =>
                       using(db)(store.read_build(_, session_name)) match {
                         case Some(build) =>