# HG changeset patch
# User wenzelm
# Date 1693138948 -7200
# Node ID e92bbd5fd66f2b9cc40c43d10a8bec2b5034f472
# Parent  cf114894a5ed6b414abf34a11a005237de2d8c3f
more robust access to local variables;

diff -r cf114894a5ed -r e92bbd5fd66f src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sun Aug 27 13:15:32 2023 +0200
+++ b/src/Pure/System/progress.scala	Sun Aug 27 14:22:28 2023 +0200
@@ -370,7 +370,7 @@
     body
   }
 
-  private def sync_database[A](body: => A): A = {
+  private def sync_database[A](body: => A): A = synchronized {
     Progress.private_data.transaction_lock(db, label = "Database_Progress.sync_database") {
       _stopped_db = Progress.private_data.read_progress_stopped(db, _context)