# HG changeset patch # User wenzelm # Date 1692643215 -7200 # Node ID 131e2a220c78f14b6ac3abc62f66160a9007e061 # Parent 20360824863a21d527c4e00d6abb40c755b46164 proper sequential evaluation; diff -r 20360824863a -r 131e2a220c78 src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Mon Aug 21 15:54:08 2023 +0200 +++ b/src/Pure/General/sql.scala Mon Aug 21 20:40:15 2023 +0200 @@ -481,7 +481,10 @@ 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; "\nnow = " + (Time.now() - time_start).toString + "\n" } + time_start + 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) }