src/Pure/General/output.scala

--- a/src/Pure/General/output.scala	Wed Apr 01 18:19:46 2020 +0200
+++ b/src/Pure/General/output.scala	Wed Apr 01 18:22:19 2020 +0200
@@ -15,11 +15,11 @@
 
   def writeln_text(msg: String): String = clean_yxml(msg)
 
-  def warning_text(msg: String): String =
-    Library.prefix_lines("### ", clean_yxml(msg))
+  def warning_prefix(s: String): String = Library.prefix_lines("### ", s)
+  def warning_text(msg: String): String = warning_prefix(clean_yxml(msg))
 
-  def error_message_text(msg: String): String =
-    Library.prefix_lines("*** ", clean_yxml(msg))
+  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)
   {