# HG changeset patch
# User wenzelm
# Date 1689503681 -7200
# Node ID b625cdabf963389a1a0d99ef9c9402d10b3dad1d
# Parent  1f074427ad2b62271e437cb0875993a4690eccf6
tuned output;

diff -r 1f074427ad2b -r b625cdabf963 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Jul 16 12:34:30 2023 +0200
+++ b/src/Pure/General/sql.scala	Sun Jul 16 12:34:41 2023 +0200
@@ -476,18 +476,20 @@
 
       val trace_count = transaction_count()
       val trace_start = Time.now()
+      var trace_nl = false
 
-      def trace(msg: => String, nl: Boolean = false): Unit = {
+      def trace(msg: String, nl: Boolean = false): Unit = {
         val trace_time = Time.now() - trace_start
         if (trace_time >= trace_min) {
-          log((if (nl) "\n" else "") + trace_time + " transaction " +
-            (if (label.isEmpty) "" else label + " ") + trace_count + ": " + msg)
+          val nl = if (trace_nl) { trace_nl = true; "\n" } else ""
+          log(nl + trace_time + " transaction " + trace_count +
+            if_proper(label, " " + label) + ": " + msg)
         }
       }
 
       val res =
         transaction {
-          trace("begin", nl = true)
+          trace("begin")
           if (tables.lock(db, create = create)) trace("locked")
           val res = Exn.capture { body }
           trace("end")