# HG changeset patch
# User wenzelm
# Date 1687783722 -7200
# Node ID f4f441edafca2bd69266ef9373888a09b3be7cfa
# Parent  a40ae2df39ad9a6f7ed2614bec5137a5622a0f80
tuned;

diff -r a40ae2df39ad -r f4f441edafca src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Mon Jun 26 13:20:12 2023 +0200
+++ b/src/Pure/Thy/export.scala	Mon Jun 26 14:48:42 2023 +0200
@@ -250,10 +250,8 @@
 
   /* context for database access */
 
-  def open_database_context(store: Store): Database_Context = {
-    val database_server = if (store.build_database_server) Some(store.open_database_server()) else None
-    new Database_Context(store, database_server)
-  }
+  def open_database_context(store: Store): Database_Context =
+    new Database_Context(store, store.maybe_open_database_server())
 
   def open_session_context0(store: Store, session: String): Session_Context =
     open_database_context(store).open_session0(session, close_database_context = true)