src/Pure/System/progress.scala
changeset 72663 e9030100f97d
parent 72599 76550282267f
child 72664 0d3224b3a92c
equal deleted inserted replaced
72662:5c08ad7adf77 72663:e9030100f97d
    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(path: Path) { echo("Document at " + path.absolute) }
    35   def echo_document(msg: String) { echo(Output.error_message_text(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