# HG changeset patch
# User wenzelm
# Date 1494774057 -7200
# Node ID 0b8a6a62114fe9a1e571321662d10a564a609d89
# Parent  11f87ab51ddb36a88ca3087096597d179cf6466a
clarified interface;

diff -r 11f87ab51ddb -r 0b8a6a62114f src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sun May 14 16:54:03 2017 +0200
+++ b/src/Pure/System/progress.scala	Sun May 14 17:00:57 2017 +0200
@@ -16,6 +16,9 @@
   def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
   def theory(session: String, theory: String) {}
 
+  def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
+  def echo_error(msg: String) { echo(Output.error_text(msg)) }
+
   def stopped: Boolean = false
   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"