# HG changeset patch
# User wenzelm
# Date 1689527588 -7200
# Node ID ba71ea02d9651562323ab74ee0b2e69cb0567150
# Parent  6689b4c07bba7c74c91b0b71bd7d2575ad54612e
more robust Java/Scala multithreading: transaction is always connection.synchronized;

diff -r 6689b4c07bba -r ba71ea02d965 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Jul 16 16:12:38 2023 +0200
+++ b/src/Pure/General/sql.scala	Sun Jul 16 19:13:08 2023 +0200
@@ -257,11 +257,9 @@
       db: Database,
       create: Boolean = false,
       label: String = "",
-      log: Logger = new System_Logger,
-      synchronized: Boolean = false,
+      log: Logger = new System_Logger
     )(body: => A): A = {
-      def run: A = db.transaction_lock(tables, create = create, label = label, log = log)(body)
-      if (synchronized) db.synchronized { run } else run
+      db.transaction_lock(tables, create = create, label = label, log = log)(body)
     }
 
     def make_table(columns: List[Column], body: String = "", name: String = ""): Table = {
@@ -440,7 +438,7 @@
 
     override def close(): Unit = connection.close()
 
-    def transaction[A](body: => A): A = {
+    def transaction[A](body: => A): A = connection.synchronized {
       val auto_commit = connection.getAutoCommit()
       try {
         connection.setAutoCommit(false)
diff -r 6689b4c07bba -r ba71ea02d965 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Sun Jul 16 16:12:38 2023 +0200
+++ b/src/Pure/ML/ml_heap.scala	Sun Jul 16 19:13:08 2023 +0200
@@ -123,12 +123,12 @@
   }
 
   def clean_entry(db: SQL.Database, session_name: String): Unit =
-    Data.transaction_lock(db, create = true, synchronized = true, label = "ML_Heap.clean_entry") {
+    Data.transaction_lock(db, create = true, label = "ML_Heap.clean_entry") {
       Data.clean_entry(db, session_name)
     }
 
   def get_entry(db: SQL.Database, session_name: String): Option[SHA1.Digest] =
-    Data.transaction_lock(db, create = true, synchronized = true, label = "ML_Heap.get_entry") {
+    Data.transaction_lock(db, create = true, label = "ML_Heap.get_entry") {
       Data.get_entry(db, session_name)
     }
 
@@ -149,7 +149,7 @@
         val step = (size.toDouble / slices.toDouble).ceil.toLong
 
         try {
-          Data.transaction_lock(db, create = true, synchronized = true, label = "ML_Heap.store1") {
+          Data.transaction_lock(db, create = true, label = "ML_Heap.store1") {
             Data.prepare_entry(db, session_name)
           }
 
@@ -160,17 +160,17 @@
             val content =
               Bytes.read_file(heap.file, offset = offset, limit = limit)
                 .compress(cache = cache)
-            Data.transaction_lock(db, synchronized = true, label = "ML_Heap.store2") {
+            Data.transaction_lock(db, label = "ML_Heap.store2") {
               Data.write_entry(db, session_name, i, content)
             }
           }
 
-          Data.transaction_lock(db, synchronized = true, label = "ML_Heap.store3") {
+          Data.transaction_lock(db, label = "ML_Heap.store3") {
             Data.finish_entry(db, session_name, size, digest)
           }
         }
         catch { case exn: Throwable =>
-          Data.transaction_lock(db, create = true, synchronized = true, label = "ML_Heap.store4") {
+          Data.transaction_lock(db, create = true, label = "ML_Heap.store4") {
             Data.clean_entry(db, session_name)
           }
           throw exn
@@ -188,7 +188,7 @@
     database match {
       case None =>
       case Some(db) =>
-        Data.transaction_lock(db, create = true, synchronized = true, label = "ML_Heap.restore") {
+        Data.transaction_lock(db, create = true, label = "ML_Heap.restore") {
           val db_digest = Data.get_entry(db, session_name)
           val file_digest = read_file_digest(heap)
 
diff -r 6689b4c07bba -r ba71ea02d965 src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Sun Jul 16 16:12:38 2023 +0200
+++ b/src/Pure/Thy/store.scala	Sun Jul 16 19:13:08 2023 +0200
@@ -423,11 +423,7 @@
     Export.clean_session(db, name)
     Document_Build.clean_session(db, name)
 
-    Store.Data.transaction_lock(db,
-      create = true,
-      synchronized = true,
-      label = "Store.clean_session_info"
-    ) {
+    Store.Data.transaction_lock(db, create = true, label = "Store.clean_session_info") {
       val already_defined = session_info_defined(db, name)
 
       db.execute_statement(
@@ -448,7 +444,7 @@
     build_log: Build_Log.Session_Info,
     build: Store.Build_Info
   ): Unit = {
-    Store.Data.transaction_lock(db, synchronized = true, label = "Store.write_session_info") {
+    Store.Data.transaction_lock(db, label = "Store.write_session_info") {
       Store.Data.write_sources(db, session_name, sources)
       Store.Data.write_session_info(db, cache.compress, session_name, build_log, build)
     }