# HG changeset patch
# User wenzelm
# Date 1689516672 -7200
# Node ID 4978a158dc4c277166b6c703d2aac94051381be5
# Parent  aa4ea5398ab84017414ca2980980ab609128a474
tuned signature;

diff -r aa4ea5398ab8 -r 4978a158dc4c src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sun Jul 16 15:53:13 2023 +0200
+++ b/src/Pure/Thy/export.scala	Sun Jul 16 16:11:12 2023 +0200
@@ -332,7 +332,8 @@
           case Some(db) => session_hierarchy.map(name => new Session_Database(name, db))
           case None =>
             val attempts =
-              session_hierarchy.map(name => name -> store.try_open_database(name, server = false))
+              for (name <- session_hierarchy)
+                yield name -> store.try_open_database(name, server_mode = false)
             attempts.collectFirst({ case (name, None) => name }) match {
               case Some(bad) =>
                 for ((_, Some(db)) <- attempts) db.close()
diff -r aa4ea5398ab8 -r 4978a158dc4c src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Sun Jul 16 15:53:13 2023 +0200
+++ b/src/Pure/Thy/store.scala	Sun Jul 16 16:11:12 2023 +0200
@@ -327,12 +327,12 @@
   def try_open_database(
     name: String,
     output: Boolean = false,
-    server: Boolean = build_database_server
+    server_mode: Boolean = build_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 (server) check(open_database_server())
+    if (server_mode) check(open_database_server())
     else if (output) Some(SQLite.open_database(output_database(name)))
     else {
       (for {