# HG changeset patch
# User wenzelm
# Date 1725631188 -7200
# Node ID e31ebb2be43724192f7b4f86fb27fc4b27192c07
# Parent  774e5a0c4c9eedbd96af29bb7462d29c8a006655
clarified signature;

diff -r 774e5a0c4c9e -r e31ebb2be437 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Fri Sep 06 15:46:51 2024 +0200
+++ b/src/Pure/Admin/build_history.scala	Fri Sep 06 15:59:48 2024 +0200
@@ -342,7 +342,7 @@
             else Nil
           for (msg <- errors)
           yield {
-            val content = Library.encode_lines(Output.clean_yxml(msg))
+            val content = Library.encode_lines(Protocol_Message.clean_output(msg))
             List(Build_Log.SESSION_NAME -> session_name, Markup.CONTENT -> content)
           }
         }
diff -r 774e5a0c4c9e -r e31ebb2be437 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Fri Sep 06 15:46:51 2024 +0200
+++ b/src/Pure/Build/build.scala	Fri Sep 06 15:59:48 2024 +0200
@@ -793,8 +793,8 @@
 
     def check(filter: List[Regex], make_string: => String): Boolean =
       filter.isEmpty || {
-        val s = Output.clean_yxml(make_string)
-        filter.forall(r => r.findFirstIn(Output.clean_yxml(s)).nonEmpty)
+        val s = Protocol_Message.clean_output(make_string)
+        filter.forall(r => r.findFirstIn(Protocol_Message.clean_output(s)).nonEmpty)
       }
 
     def print(session_name: String): Unit = {
diff -r 774e5a0c4c9e -r e31ebb2be437 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Fri Sep 06 15:46:51 2024 +0200
+++ b/src/Pure/GUI/gui.scala	Fri Sep 06 15:59:48 2024 +0200
@@ -72,7 +72,7 @@
     height: Int = 20,
     editable: Boolean = false
   ) : ScrollPane = {
-    val txt = Output.clean_yxml(raw_txt)
+    val txt = Protocol_Message.clean_output(raw_txt)
     val text = new TextArea(txt)
     if (width > 0) text.columns = width
     if (height > 0 && split_lines(txt).length > height) text.rows = height
diff -r 774e5a0c4c9e -r e31ebb2be437 src/Pure/General/output.scala
--- a/src/Pure/General/output.scala	Fri Sep 06 15:46:51 2024 +0200
+++ b/src/Pure/General/output.scala	Fri Sep 06 15:59:48 2024 +0200
@@ -8,17 +8,14 @@
 
 
 object Output {
-  def clean_yxml(msg: String): String =
-    try { XML.content(Protocol_Message.clean_reports(YXML.parse_body(YXML.Source(msg)))) }
-    catch { case ERROR(_) => msg }
-
-  def writeln_text(msg: String): String = clean_yxml(msg)
+  def writeln_text(msg: String): String = Protocol_Message.clean_output(msg)
 
   def warning_prefix(s: String): String = Library.prefix_lines("### ", s)
-  def warning_text(msg: String): String = warning_prefix(clean_yxml(msg))
+  def warning_text(msg: String): String = warning_prefix(Protocol_Message.clean_output(msg))
 
   def error_message_prefix(s: String): String = Library.prefix_lines("*** ", s)
-  def error_message_text(msg: String): String = error_message_prefix(clean_yxml(msg))
+  def error_message_text(msg: String): String =
+    error_message_prefix(Protocol_Message.clean_output(msg))
 
   def output(s: String, stdout: Boolean = false, include_empty: Boolean = false): Unit =
     if (s.nonEmpty || include_empty) {
diff -r 774e5a0c4c9e -r e31ebb2be437 src/Pure/PIDE/protocol_message.scala
--- a/src/Pure/PIDE/protocol_message.scala	Fri Sep 06 15:46:51 2024 +0200
+++ b/src/Pure/PIDE/protocol_message.scala	Fri Sep 06 15:59:48 2024 +0200
@@ -55,4 +55,11 @@
       case XML.Elem(_, ts) => reports(props, ts)
       case XML.Text(_) => Nil
     }
+
+
+  /* clean output */
+
+  def clean_output(msg: String): String =
+    try { XML.content(clean_reports(YXML.parse_body(YXML.Source(msg)))) }
+    catch { case ERROR(_) => msg }
 }
diff -r 774e5a0c4c9e -r e31ebb2be437 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Fri Sep 06 15:46:51 2024 +0200
+++ b/src/Pure/Tools/dump.scala	Fri Sep 06 15:59:48 2024 +0200
@@ -327,7 +327,7 @@
         val bad_theories = Consumer.shutdown()
         val bad_msgs =
           bad_theories.map(bad =>
-            Output.clean_yxml(
+            Protocol_Message.clean_output(
               "FAILED theory " + bad.name +
                 (if (bad.status.consolidated) "" else ": " + bad.status.percentage + "% finished") +
                 if_proper(bad.errors, bad.errors.mkString("\n", "\n", ""))))