# HG changeset patch
# User wenzelm
# Date 1692609887 -7200
# Node ID 7f564f33172b3c1d78bb08c863f51806092b7533
# Parent  e3ae7293c5df356c93ccccea1d6dee47f9d9b861
tuned messages;

diff -r e3ae7293c5df -r 7f564f33172b src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon Aug 21 11:15:25 2023 +0200
+++ b/src/Pure/General/sql.scala	Mon Aug 21 11:24:47 2023 +0200
@@ -19,6 +19,8 @@
 
 
 object SQL {
+  lazy val time_start = Time.now()
+
   /** SQL language **/
 
   type Source = String
@@ -479,7 +481,7 @@
       def trace(msg: String): Unit = {
         val trace_time = Time.now() - trace_start
         if (trace_time >= trace_min) {
-          val nl = if (trace_nl) "" else { trace_nl = true; "\n" }
+          val nl = if (trace_nl) "" else { trace_nl = true; "\nnow = " + (Time.now() - time_start).toString + "\n" }
           log(nl + trace_time + " transaction " + trace_count +
             if_proper(label, " " + label) + ": " + msg)
         }