# HG changeset patch
# User wenzelm
# Date 1659787589 -7200
# Node ID 70a65ee4a738e50d3838e8ff2c0587d3c8335df5
# Parent  efc25bf4b795f9b8b0523cc6d790399de075104a
clarified signature: more robust treatment of server;

diff -r efc25bf4b795 -r 70a65ee4a738 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Aug 05 22:49:25 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sat Aug 06 14:06:29 2022 +0200
@@ -299,7 +299,8 @@
           case Some(db) => session_hierarchy.map(name => new Session_Database(name, db))
           case None =>
             val store = db_context.store
-            val attempts = session_hierarchy.map(name => name -> store.try_open_database(name))
+            val attempts =
+              session_hierarchy.map(name => name -> store.try_open_database(name, server = false))
             attempts.collectFirst({ case (name, None) => name }) match {
               case Some(bad) =>
                 for ((_, Some(db)) <- attempts) db.close()
diff -r efc25bf4b795 -r 70a65ee4a738 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Aug 05 22:49:25 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 06 14:06:29 2022 +0200
@@ -1356,14 +1356,18 @@
               port = options.int("build_database_ssh_port"))),
         ssh_close = true)
 
-    def open_database_context(): Database_Context =
-      new Database_Context(store, if (database_server) Some(open_database_server()) else None)
+    def open_database_context(server: Boolean = database_server): Database_Context =
+      new Database_Context(store, if (server) Some(open_database_server()) else None)
 
-    def try_open_database(name: String, output: Boolean = false): Option[SQL.Database] = {
+    def try_open_database(
+      name: String,
+      output: Boolean = false,
+      server: Boolean = database_server
+    ): Option[SQL.Database] = {
       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())
+      if (server) check(open_database_server())
       else if (output) Some(SQLite.open_database(output_database(name)))
       else {
         (for {