equal
deleted
inserted
replaced
30 def theory(theory: Progress.Theory) {} |
30 def theory(theory: Progress.Theory) {} |
31 def nodes_status(nodes_status: Document_Status.Nodes_Status) {} |
31 def nodes_status(nodes_status: Document_Status.Nodes_Status) {} |
32 |
32 |
33 def echo_warning(msg: String) { echo(Output.warning_text(msg)) } |
33 def echo_warning(msg: String) { echo(Output.warning_text(msg)) } |
34 def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) } |
34 def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) } |
35 def echo_document(msg: String) { echo(Output.error_message_text(msg)) } |
35 def echo_document(msg: String) { echo(msg) } |
36 |
36 |
37 def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A = |
37 def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A = |
38 Timing.timeit(message, enabled, echo)(e) |
38 Timing.timeit(message, enabled, echo)(e) |
39 |
39 |
40 @volatile protected var is_stopped = false |
40 @volatile protected var is_stopped = false |