# HG changeset patch
# User wenzelm
# Date 1689618739 -7200
# Node ID d032bf604e9389940b28ce8853acd11cbb70ac54
# Parent  6c211e1c94d5881ee65aac176bbd0fcb6edaebad
more robust: exclude accidental nesting (synchronized block is re-entrant);

diff -r 6c211e1c94d5 -r d032bf604e93 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon Jul 17 20:31:45 2023 +0200
+++ b/src/Pure/General/sql.scala	Mon Jul 17 20:32:19 2023 +0200
@@ -439,7 +439,7 @@
     override def close(): Unit = connection.close()
 
     def transaction[A](body: => A): A = connection.synchronized {
-      val auto_commit = connection.getAutoCommit()
+      require(connection.getAutoCommit(), "transaction already active")
       try {
         connection.setAutoCommit(false)
         val savepoint = connection.setSavepoint()
@@ -450,7 +450,7 @@
         }
         catch { case exn: Throwable => connection.rollback(savepoint); throw exn }
       }
-      finally { connection.setAutoCommit(auto_commit) }
+      finally { connection.setAutoCommit(true) }
     }
 
     def transaction_lock[A](