# HG changeset patch
# User wenzelm
# Date 1677673835 -3600
# Node ID 0030eabbe6c3d68c3fb5f9c69d9e5a59773ef52c
# Parent  dcbf96acae274aeabdecd064f6ac8c73cd9e36c9
more robust: synchronized access to database;

diff -r dcbf96acae27 -r 0030eabbe6c3 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 13:23:49 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 13:30:35 2023 +0100
@@ -544,18 +544,16 @@
     }
 
   private def setup_database(): Unit =
-    for (db <- _database) {
-      synchronized {
-        db.transaction {
-          Build_Process.Data.init_database(db, build_context)
-        }
+    synchronized {
+      for (db <- _database) {
+        db.transaction { Build_Process.Data.init_database(db, build_context) }
+        db.rebuild()
       }
-      db.rebuild()
     }
 
   private def sync_database(): Unit =
-    for (db <- _database) {
-      synchronized {
+    synchronized {
+      for (db <- _database) {
         db.transaction {
           _state =
             Build_Process.Data.update_database(
@@ -564,7 +562,8 @@
       }
     }
 
-  def close(): Unit = _database.foreach(_.close())
+  def close(): Unit =
+    synchronized { _database.foreach(_.close()) }
 
 
   /* policy operations */