# HG changeset patch
# User wenzelm
# Date 1678310555 -3600
# Node ID 3f3dcf9f53f1a87aeaaea96775407da905565c6f
# Parent  edc96be6b939f743e7f6f1676160d5ed4831ae40
more robust transactions;

diff -r edc96be6b939 -r 3f3dcf9f53f1 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Wed Mar 08 22:08:48 2023 +0100
+++ b/src/Pure/General/sql.scala	Wed Mar 08 22:22:35 2023 +0100
@@ -490,7 +490,9 @@
     host: String = "",
     port: Int = 0,
     ssh: Option[SSH.Session] = None,
-    ssh_close: Boolean = false
+    ssh_close: Boolean = false,
+    // see https://www.postgresql.org/docs/current/transaction-iso.html
+    transaction_isolation: Int = Connection.TRANSACTION_SERIALIZABLE
   ): Database = {
     init_jdbc
 
@@ -518,6 +520,7 @@
       }
     try {
       val connection = DriverManager.getConnection(url, user, password)
+      connection.setTransactionIsolation(transaction_isolation)
       new Database(name, connection, port_forwarding)
     }
     catch { case exn: Throwable => port_forwarding.foreach(_.close()); throw exn }