1/* Title: Pure/General/output.scala 2 Author: Makarius 3 4Isabelle output channels. 5*/ 6 7package isabelle 8 9 10object Output 11{ 12 def clean_yxml(msg: String): String = 13 try { XML.content(Protocol_Message.clean_reports(YXML.parse_body(msg))) } 14 catch { case ERROR(_) => msg } 15 16 def writeln_text(msg: String): String = clean_yxml(msg) 17 18 def warning_text(msg: String): String = 19 Library.prefix_lines("### ", clean_yxml(msg)) 20 21 def error_message_text(msg: String): String = 22 Library.prefix_lines("*** ", clean_yxml(msg)) 23 24 def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false) 25 { 26 if (msg.nonEmpty || include_empty) { 27 if (stdout) Console.print(writeln_text(msg) + "\n") 28 else Console.err.print(writeln_text(msg) + "\n") 29 } 30 } 31 32 def warning(msg: String, stdout: Boolean = false, include_empty: Boolean = false) 33 { 34 if (msg.nonEmpty || include_empty) { 35 if (stdout) Console.print(warning_text(msg) + "\n") 36 else Console.err.print(warning_text(msg) + "\n") 37 } 38 } 39 40 def error_message(msg: String, stdout: Boolean = false, include_empty: Boolean = false) 41 { 42 if (msg.nonEmpty || include_empty) { 43 if (stdout) Console.print(error_message_text(msg) + "\n") 44 else Console.err.print(error_message_text(msg) + "\n") 45 } 46 } 47} 48