src/Pure/General/output.scala
changeset 67178 70576478bda9
parent 65828 02dd430d80c5
     1.1 --- a/src/Pure/General/output.scala	Sun Dec 10 18:43:08 2017 +0100
     1.2 +++ b/src/Pure/General/output.scala	Sun Dec 10 20:29:00 2017 +0100
     1.3 @@ -24,24 +24,24 @@
     1.4    def writeln(msg: String, stdout: Boolean = false)
     1.5    {
     1.6      if (msg != "") {
     1.7 -      if (stdout) Console.println(writeln_text(msg))
     1.8 -      else Console.err.println(writeln_text(msg))
     1.9 +      if (stdout) Console.print(writeln_text(msg) + "\n")
    1.10 +      else Console.err.print(writeln_text(msg) + "\n")
    1.11      }
    1.12    }
    1.13  
    1.14    def warning(msg: String, stdout: Boolean = false)
    1.15    {
    1.16      if (msg != "") {
    1.17 -      if (stdout) Console.println(warning_text(msg))
    1.18 -      else Console.err.println(warning_text(msg))
    1.19 +      if (stdout) Console.print(warning_text(msg) + "\n")
    1.20 +      else Console.err.print(warning_text(msg) + "\n")
    1.21      }
    1.22    }
    1.23  
    1.24    def error_message(msg: String, stdout: Boolean = false)
    1.25    {
    1.26      if (msg != "") {
    1.27 -      if (stdout) Console.println(error_message_text(msg))
    1.28 -      else Console.err.println(error_message_text(msg))
    1.29 +      if (stdout) Console.print(error_message_text(msg) + "\n")
    1.30 +      else Console.err.print(error_message_text(msg) + "\n")
    1.31      }
    1.32    }
    1.33  }