src/Pure/General/sql.scala
changeset 78361 b625cdabf963
parent 78358 f5cf8e500dee
child 78362 8da30ae02dda
equal deleted inserted replaced
78360:1f074427ad2b 78361:b625cdabf963
   474           case s => error("Bad system property " + prop + ": " + quote(s))
   474           case s => error("Bad system property " + prop + ": " + quote(s))
   475         }
   475         }
   476 
   476 
   477       val trace_count = transaction_count()
   477       val trace_count = transaction_count()
   478       val trace_start = Time.now()
   478       val trace_start = Time.now()
   479 
   479       var trace_nl = false
   480       def trace(msg: => String, nl: Boolean = false): Unit = {
   480 
       
   481       def trace(msg: String, nl: Boolean = false): Unit = {
   481         val trace_time = Time.now() - trace_start
   482         val trace_time = Time.now() - trace_start
   482         if (trace_time >= trace_min) {
   483         if (trace_time >= trace_min) {
   483           log((if (nl) "\n" else "") + trace_time + " transaction " +
   484           val nl = if (trace_nl) { trace_nl = true; "\n" } else ""
   484             (if (label.isEmpty) "" else label + " ") + trace_count + ": " + msg)
   485           log(nl + trace_time + " transaction " + trace_count +
       
   486             if_proper(label, " " + label) + ": " + msg)
   485         }
   487         }
   486       }
   488       }
   487 
   489 
   488       val res =
   490       val res =
   489         transaction {
   491         transaction {
   490           trace("begin", nl = true)
   492           trace("begin")
   491           if (tables.lock(db, create = create)) trace("locked")
   493           if (tables.lock(db, create = create)) trace("locked")
   492           val res = Exn.capture { body }
   494           val res = Exn.capture { body }
   493           trace("end")
   495           trace("end")
   494           res
   496           res
   495         }
   497         }