src/Pure/General/output.scala
changeset 73340 0ffcad1f6130
parent 71647 7b0656fa783b
child 75393 87ebf5a50283
equal deleted inserted replaced
73339:9efdebe24c65 73340:0ffcad1f6130
    19   def warning_text(msg: String): String = warning_prefix(clean_yxml(msg))
    19   def warning_text(msg: String): String = warning_prefix(clean_yxml(msg))
    20 
    20 
    21   def error_prefix(s: String): String = Library.prefix_lines("*** ", s)
    21   def error_prefix(s: String): String = Library.prefix_lines("*** ", s)
    22   def error_message_text(msg: String): String = error_prefix(clean_yxml(msg))
    22   def error_message_text(msg: String): String = error_prefix(clean_yxml(msg))
    23 
    23 
    24   def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
    24   def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit =
    25   {
    25   {
    26     if (msg.nonEmpty || include_empty) {
    26     if (msg.nonEmpty || include_empty) {
    27       if (stdout) Console.print(writeln_text(msg) + "\n")
    27       if (stdout) Console.print(writeln_text(msg) + "\n")
    28       else Console.err.print(writeln_text(msg) + "\n")
    28       else Console.err.print(writeln_text(msg) + "\n")
    29     }
    29     }
    30   }
    30   }
    31 
    31 
    32   def warning(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
    32   def warning(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit =
    33   {
    33   {
    34     if (msg.nonEmpty || include_empty) {
    34     if (msg.nonEmpty || include_empty) {
    35       if (stdout) Console.print(warning_text(msg) + "\n")
    35       if (stdout) Console.print(warning_text(msg) + "\n")
    36       else Console.err.print(warning_text(msg) + "\n")
    36       else Console.err.print(warning_text(msg) + "\n")
    37     }
    37     }
    38   }
    38   }
    39 
    39 
    40   def error_message(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
    40   def error_message(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit =
    41   {
    41   {
    42     if (msg.nonEmpty || include_empty) {
    42     if (msg.nonEmpty || include_empty) {
    43       if (stdout) Console.print(error_message_text(msg) + "\n")
    43       if (stdout) Console.print(error_message_text(msg) + "\n")
    44       else Console.err.print(error_message_text(msg) + "\n")
    44       else Console.err.print(error_message_text(msg) + "\n")
    45     }
    45     }