src/Pure/General/output.scala
changeset 71164 a21a29de5f57
parent 71100 f31903cc57b0
child 71647 7b0656fa783b
--- a/src/Pure/General/output.scala	Mon Nov 25 12:19:14 2019 +0100
+++ b/src/Pure/General/output.scala	Mon Nov 25 12:41:52 2019 +0100
@@ -16,10 +16,10 @@
   def writeln_text(msg: String): String = clean_yxml(msg)
 
   def warning_text(msg: String): String =
-    cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
+    Library.prefix_lines("### ", clean_yxml(msg))
 
   def error_message_text(msg: String): String =
-    cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
+    Library.prefix_lines("*** ", clean_yxml(msg))
 
   def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
   {