--- 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)
}
}
--- 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 = {
--- 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
--- 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) {
--- 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 }
}
--- 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", ""))))