# HG changeset patch
# User wenzelm
# Date 1689585628 -7200
# Node ID 2deecde7f1f6098ab0c845321e548b2c35e87c28
# Parent  30d3faa6c24564aee9a61a9e4b20ef07897806e0
more informative trace;

diff -r 30d3faa6c245 -r 2deecde7f1f6 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Jul 16 21:01:33 2023 +0200
+++ b/src/Pure/General/sql.scala	Mon Jul 17 11:20:28 2023 +0200
@@ -481,18 +481,21 @@
         }
       }
 
-      val res =
-        transaction {
-          trace("begin")
-          if (tables.lock(db, create = create)) {
-            trace("locked " + commas_quote(tables.list.map(_.name)), force = true)
+      try {
+        val res =
+          transaction {
+            trace("begin")
+            if (tables.lock(db, create = create)) {
+              trace("locked " + commas_quote(tables.list.map(_.name)), force = true)
+            }
+            val res = Exn.capture { body }
+            trace("end")
+            res
           }
-          val res = Exn.capture { body }
-          trace("end")
-          res
-        }
-      trace("commit")
-      Exn.release(res)
+        trace("commit")
+        Exn.release(res)
+      }
+      catch { case exn: Throwable => trace("crash"); throw exn }
     }
 
     def lock_tables(tables: List[Table]): Source = ""  // PostgreSQL only