# 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