# HG changeset patch
# User wenzelm
# Date 1689529092 -7200
# Node ID 928e031b7c52879a05f524bf9f6b02e65072686d
# Parent  fda3f7a158b952313dd12eed7d40141e1e3bdaa2
tuned output;

diff -r fda3f7a158b9 -r 928e031b7c52 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Jul 16 19:30:10 2023 +0200
+++ b/src/Pure/General/sql.scala	Sun Jul 16 19:38:12 2023 +0200
@@ -472,9 +472,9 @@
       val trace_start = Time.now()
       var trace_nl = false
 
-      def trace(msg: String, nl: Boolean = false): Unit = {
+      def trace(msg: String, nl: Boolean = false, force: Boolean = false): Unit = {
         val trace_time = Time.now() - trace_start
-        if (trace_time >= trace_min) {
+        if (trace_time >= trace_min || force) {
           val nl = if (trace_nl) "" else { trace_nl = true; "\n" }
           log(nl + trace_time + " transaction " + trace_count +
             if_proper(label, " " + label) + ": " + msg)
@@ -484,7 +484,9 @@
       val res =
         transaction {
           trace("begin")
-          if (tables.lock(db, create = create)) trace("locked")
+          if (tables.lock(db, create = create)) {
+            trace("locked " + commas_quote(tables.list.map(_.name)), force = true)
+          }
           val res = Exn.capture { body }
           trace("end")
           res