--- a/src/Pure/General/output.scala Sun Dec 10 18:43:08 2017 +0100
+++ b/src/Pure/General/output.scala Sun Dec 10 20:29:00 2017 +0100
@@ -24,24 +24,24 @@
def writeln(msg: String, stdout: Boolean = false)
{
if (msg != "") {
- if (stdout) Console.println(writeln_text(msg))
- else Console.err.println(writeln_text(msg))
+ if (stdout) Console.print(writeln_text(msg) + "\n")
+ else Console.err.print(writeln_text(msg) + "\n")
}
}
def warning(msg: String, stdout: Boolean = false)
{
if (msg != "") {
- if (stdout) Console.println(warning_text(msg))
- else Console.err.println(warning_text(msg))
+ if (stdout) Console.print(warning_text(msg) + "\n")
+ else Console.err.print(warning_text(msg) + "\n")
}
}
def error_message(msg: String, stdout: Boolean = false)
{
if (msg != "") {
- if (stdout) Console.println(error_message_text(msg))
- else Console.err.println(error_message_text(msg))
+ if (stdout) Console.print(error_message_text(msg) + "\n")
+ else Console.err.print(error_message_text(msg) + "\n")
}
}
}