src/Pure/General/output.scala

--- a/src/Pure/General/output.scala	Sat Feb 13 20:41:56 2016 +0100
+++ b/src/Pure/General/output.scala	Sat Feb 13 21:10:13 2016 +0100
@@ -18,7 +18,7 @@
   def warning_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
   def error_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
 
-  def writeln(msg: String) { Console.err.println(writeln_text(msg)) }
-  def warning(msg: String) { Console.err.println(warning_text(msg)) }
-  def error_message(msg: String) { Console.err.println(error_text(msg)) }
+  def writeln(msg: String) { if (msg != "") Console.err.println(writeln_text(msg)) }
+  def warning(msg: String) { if (msg != "") Console.err.println(warning_text(msg)) }
+  def error_message(msg: String) { if (msg != "") Console.err.println(error_text(msg)) }
 }