# HG changeset patch
# User wenzelm
# Date 1687857472 -7200
# Node ID edf86c70953546b2737a9e1c3c31e56c7af2c7c5
# Parent  fd0430a7b7a47da4980da82a1346abb6acb5eee9
more robust close() after failed initialization;

diff -r fd0430a7b7a4 -r edf86c709535 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Jun 27 10:24:32 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Tue Jun 27 11:17:52 2023 +0200
@@ -802,33 +802,40 @@
 
   /* progress backed by database */
 
+  private val _database_server: Option[SQL.Database] =
+    try { store.maybe_open_database_server() }
+    catch { case exn: Throwable => close(); throw exn }
+
   private val _build_database: Option[SQL.Database] =
-    store.maybe_open_build_database(Build_Process.Data.database)
+    try { store.maybe_open_build_database(Build_Process.Data.database) }
+    catch { case exn: Throwable => close(); throw exn }
 
   private val _host_database: Option[SQL.Database] =
-    store.maybe_open_build_database(Host.Data.database)
-
-  private val _database_server: Option[SQL.Database] =
-    store.maybe_open_database_server()
+    try { store.maybe_open_build_database(Host.Data.database) }
+    catch { case exn: Throwable => close(); throw exn }
 
   protected val (progress, worker_uuid) = synchronized {
     _build_database match {
       case None => (build_progress, UUID.random().toString)
       case Some(db) =>
-        val progress_db = store.open_build_database(Progress.Data.database)
-        val progress =
-          new Database_Progress(progress_db, build_progress,
-            hostname = hostname,
-            context_uuid = build_uuid)
-        (progress, progress.agent_uuid)
+        try {
+          val progress_db = store.open_build_database(Progress.Data.database)
+          val progress =
+            new Database_Progress(progress_db, build_progress,
+              hostname = hostname,
+              context_uuid = build_uuid)
+          (progress, progress.agent_uuid)
+        }
+        catch { case exn: Throwable => close(); throw exn }
     }
   }
 
   protected val log: Logger = Logger.make_system_log(progress, build_options)
 
   def close(): Unit = synchronized {
-    _build_database.foreach(_.close())
-    _host_database.foreach(_.close())
+    Option(_database_server).flatten.foreach(_.close())
+    Option(_build_database).flatten.foreach(_.close())
+    Option(_host_database).flatten.foreach(_.close())
     progress match {
       case db_progress: Database_Progress =>
         db_progress.exit()