more robust: assume that database is exclusive for this Progress instance --- always close on exit (see also bf377e10ff3b);

--- a/src/Pure/Build/build_process.scala	Sun Mar 03 17:47:50 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Mon Mar 04 11:05:36 2024 +0100
@@ -935,7 +935,7 @@
     Option(_host_database).foreach(_.close())
     Option(_build_cluster).foreach(_.close())
     progress match {
-      case db_progress: Database_Progress => db_progress.exit(close = true)
+      case db_progress: Database_Progress => db_progress.close()
       case _ =>
     }
   }

--- a/src/Pure/System/progress.scala	Sun Mar 03 17:47:50 2024 +0100
+++ b/src/Pure/System/progress.scala	Mon Mar 04 11:05:36 2024 +0100
@@ -378,7 +378,7 @@
         (results, true) })
   }
 
-  def exit(close: Boolean = false): Unit = synchronized {
+  def close(): Unit = synchronized {
     if (_context > 0) {
       _consumer.shutdown()
       _consumer = null
@@ -388,7 +388,7 @@
       }
       _context = 0
     }
-    if (close) db.close()
+    db.close()
   }
 
   private def sync_context[A](body: => A): A = synchronized {