# HG changeset patch
# User wenzelm
# Date 1486721752 -3600
# Node ID cda3d36aceb2873dbbfe813008c79496ce6c4df9
# Parent  da8ae577d171d22df8648aba88a269019b02bbbb
proper transaction for PostgreSQL;

diff -r da8ae577d171 -r cda3d36aceb2 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Fri Feb 10 11:04:28 2017 +0100
+++ b/src/Pure/General/sql.scala	Fri Feb 10 11:15:52 2017 +0100
@@ -173,15 +173,16 @@
     def transaction[A](body: => A): A =
     {
       val auto_commit = connection.getAutoCommit
-      val savepoint = connection.setSavepoint
-
       try {
         connection.setAutoCommit(false)
-        val result = body
-        connection.commit
-        result
+        val savepoint = connection.setSavepoint
+        try {
+          val result = body
+          connection.commit
+          result
+        }
+        catch { case exn: Throwable => connection.rollback(savepoint); throw exn }
       }
-      catch { case exn: Throwable => connection.rollback(savepoint); throw exn }
       finally { connection.setAutoCommit(auto_commit) }
     }
 
@@ -208,6 +209,7 @@
     { stmt.setBinaryStream(i, bytes.stream(), bytes.length) }
     def set_date(stmt: PreparedStatement, i: Int, date: Date)
 
+
     /* output */
 
     def bool(rs: ResultSet, name: String): Boolean = rs.getBoolean(name)