--- a/src/Pure/General/output.scala Mon Mar 07 22:36:44 2016 +0100
+++ b/src/Pure/General/output.scala Mon Mar 07 22:37:31 2016 +0100
@@ -18,7 +18,27 @@
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) { 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)) }
+ def writeln(msg: String, stdout: Boolean = false)
+ {
+ if (msg != "") {
+ if (stdout) Console.println(writeln_text(msg))
+ else Console.err.println(writeln_text(msg))
+ }
+ }
+
+ def warning(msg: String, stdout: Boolean = false)
+ {
+ if (msg != "") {
+ if (stdout) Console.println(warning_text(msg))
+ else Console.err.println(warning_text(msg))
+ }
+ }
+
+ def error_message(msg: String, stdout: Boolean = false)
+ {
+ if (msg != "") {
+ if (stdout) Console.println(error_text(msg))
+ else Console.err.println(error_text(msg))
+ }
+ }
}