src/Pure/General/sql.scala

--- a/src/Pure/General/sql.scala	Mon Jun 26 14:48:42 2023 +0200
+++ b/src/Pure/General/sql.scala	Mon Jun 26 22:15:56 2023 +0200
@@ -253,8 +253,12 @@
     def transaction_lock[A](
       db: Database,
       more_tables: Tables = Tables.empty,
-      create: Boolean = false
-    )(body: => A): A = db.transaction { (tables ::: more_tables).lock(db, create = create); body }
+      create: Boolean = false,
+      synchronized: Boolean = false,
+    )(body: => A): A = {
+      def run: A = db.transaction { (tables ::: more_tables).lock(db, create = create); body }
+      if (synchronized) db.synchronized { run } else run
+    }
 
     def vacuum(db: Database, more_tables: Tables = Tables.empty): Unit =
       db.vacuum(tables = tables ::: more_tables)