--- a/src/Pure/General/output.scala Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Pure/General/output.scala Fri Apr 01 17:06:10 2022 +0200
@@ -7,8 +7,7 @@
package isabelle
-object Output
-{
+object Output {
def clean_yxml(msg: String): String =
try { XML.content(Protocol_Message.clean_reports(YXML.parse_body(msg))) }
catch { case ERROR(_) => msg }
@@ -21,24 +20,21 @@
def error_prefix(s: String): String = Library.prefix_lines("*** ", s)
def error_message_text(msg: String): String = error_prefix(clean_yxml(msg))
- def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit =
- {
+ def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit = {
if (msg.nonEmpty || include_empty) {
if (stdout) Console.print(writeln_text(msg) + "\n")
else Console.err.print(writeln_text(msg) + "\n")
}
}
- def warning(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit =
- {
+ def warning(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit = {
if (msg.nonEmpty || include_empty) {
if (stdout) Console.print(warning_text(msg) + "\n")
else Console.err.print(warning_text(msg) + "\n")
}
}
- def error_message(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit =
- {
+ def error_message(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit = {
if (msg.nonEmpty || include_empty) {
if (stdout) Console.print(error_message_text(msg) + "\n")
else Console.err.print(error_message_text(msg) + "\n")