# HG changeset patch
# User wenzelm
# Date 1686842969 -7200
# Node ID 5454bec8f5c67814f8bb7c1bb78161220083c68b
# Parent  c6d4b1a00ad703a230bc32340d821e259b556c2d
tuned signature;

diff -r c6d4b1a00ad7 -r 5454bec8f5c6 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Thu Jun 15 17:24:32 2023 +0200
+++ b/src/Pure/Thy/export.scala	Thu Jun 15 17:29:29 2023 +0200
@@ -251,7 +251,7 @@
   /* context for database access */
 
   def open_database_context(store: Sessions.Store): Database_Context = {
-    val database_server = if (store.database_server) Some(store.open_database_server()) else None
+    val database_server = if (store.build_database_server) Some(store.open_database_server()) else None
     new Database_Context(store, database_server)
   }
 
diff -r c6d4b1a00ad7 -r 5454bec8f5c6 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Jun 15 17:24:32 2023 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Jun 15 17:29:29 2023 +0200
@@ -1495,7 +1495,7 @@
     def find_database(name: String): Option[Path] =
       input_dirs.map(_ + database(name)).find(_.is_file)
 
-    def database_server: Boolean = options.bool("build_database_server")
+    def build_database_server: Boolean = options.bool("build_database_server")
 
     def open_database_server(): PostgreSQL.Database =
       PostgreSQL.open_database(
@@ -1516,13 +1516,13 @@
 
     def open_build_database(): Option[SQL.Database] =
       if (!options.bool("build_database_test")) None
-      else if (database_server) Some(open_database_server())
+      else if (build_database_server) Some(open_database_server())
       else Some(SQLite.open_database(build_database, restrict = true))
 
     def try_open_database(
       name: String,
       output: Boolean = false,
-      server: Boolean = database_server
+      server: 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 }
@@ -1548,7 +1548,7 @@
 
     def clean_output(name: String): Option[Boolean] = {
       val relevant_db =
-        database_server &&
+        build_database_server &&
           using_option(try_open_database(name))(init_session_info(_, name)).getOrElse(false)
 
       val del =