src/Pure/System/progress.scala
changeset 65826 0b8a6a62114f
parent 64909 8007f10195af
child 65828 02dd430d80c5
equal deleted inserted replaced
65825:11f87ab51ddb 65826:0b8a6a62114f
    13 class Progress
    13 class Progress
    14 {
    14 {
    15   def echo(msg: String) {}
    15   def echo(msg: String) {}
    16   def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
    16   def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
    17   def theory(session: String, theory: String) {}
    17   def theory(session: String, theory: String) {}
       
    18 
       
    19   def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
       
    20   def echo_error(msg: String) { echo(Output.error_text(msg)) }
    18 
    21 
    19   def stopped: Boolean = false
    22   def stopped: Boolean = false
    20   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
    23   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
    21 
    24 
    22   def bash(script: String,
    25   def bash(script: String,