src/Pure/General/sql.scala
changeset 78557 131e2a220c78
parent 78554 54991440905e
child 78561 c06a0396b09d
equal deleted inserted replaced
78556:20360824863a 78557:131e2a220c78
   479       var trace_nl = false
   479       var trace_nl = false
   480 
   480 
   481       def trace(msg: String): Unit = {
   481       def trace(msg: String): Unit = {
   482         val trace_time = Time.now() - trace_start
   482         val trace_time = Time.now() - trace_start
   483         if (trace_time >= trace_min) {
   483         if (trace_time >= trace_min) {
   484           val nl = if (trace_nl) "" else { trace_nl = true; "\nnow = " + (Time.now() - time_start).toString + "\n" }
   484           time_start
       
   485           val nl =
       
   486             if (trace_nl) ""
       
   487             else { trace_nl = true; "\nnow = " + (Time.now() - time_start).toString + "\n" }
   485           log(nl + trace_time + " transaction " + trace_count +
   488           log(nl + trace_time + " transaction " + trace_count +
   486             if_proper(label, " " + label) + ": " + msg)
   489             if_proper(label, " " + label) + ": " + msg)
   487         }
   490         }
   488       }
   491       }
   489 
   492