more robust: synchronized access to database;
authorwenzelm
Wed, 01 Mar 2023 13:30:35 +0100
changeset 77438 0030eabbe6c3
parent 77437 dcbf96acae27
child 77439 d6bf9ec39d12
more robust: synchronized access to database;
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 */