equal
deleted
inserted
replaced
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 |