# HG changeset patch
# User wenzelm
# Date 1726144699 -7200
# Node ID b71a040ab128aa5be8437a41e46602b876d2fdbd
# Parent  9a7de3f320d8570cd7a3fcf0a7fa39c988cdc10a
tuned signature: more operations;

diff -r 9a7de3f320d8 -r b71a040ab128 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Thu Sep 12 14:24:36 2024 +0200
+++ b/src/Pure/General/pretty.scala	Thu Sep 12 14:38:19 2024 +0200
@@ -100,6 +100,9 @@
 
   /* no formatting */
 
+  def output_content(pure: Boolean, output: XML.Body): String =
+    XML.content(if (pure) Protocol_Message.clean_output(output) else output)
+
   def unbreakable(input: XML.Body): XML.Body =
     input flatMap {
       case XML.Wrapped_Elem(markup, body1, body2) =>
@@ -109,8 +112,8 @@
       case XML.Text(text) => XML.string(split_lines(text).mkString(Symbol.space))
     }
 
-  def unformatted_string_of(input: XML.Body): String =
-    XML.content(unbreakable(input))
+  def unformatted_string_of(input: XML.Body, pure: Boolean = false): String =
+    output_content(pure, unbreakable(input))
 
 
   /* formatting */
@@ -207,8 +210,11 @@
   }
 
   def string_of(input: XML.Body,
-      margin: Double = default_margin,
-      breakgain: Double = default_breakgain,
-      metric: Metric = Default_Metric): String =
-    XML.content(formatted(input, margin = margin, breakgain = breakgain, metric = metric))
+    margin: Double = default_margin,
+    breakgain: Double = default_breakgain,
+    metric: Metric = Default_Metric,
+    pure: Boolean = false
+  ): String = {
+    output_content(pure, formatted(input, margin = margin, breakgain = breakgain, metric = metric))
+  }
 }
diff -r 9a7de3f320d8 -r b71a040ab128 src/Pure/PIDE/protocol_message.scala
--- a/src/Pure/PIDE/protocol_message.scala	Thu Sep 12 14:24:36 2024 +0200
+++ b/src/Pure/PIDE/protocol_message.scala	Thu Sep 12 14:38:19 2024 +0200
@@ -60,12 +60,10 @@
 
   /* clean output */
 
+  def clean_output(xml: XML.Body): XML.Body =
+    XML.filter_elements(xml, remove = report_elements, expose = no_report_elements)
+
   def clean_output(msg: String): String =
-    try {
-      XML.content(
-        XML.filter_elements(YXML.parse_body(YXML.Source(msg)),
-          remove = report_elements,
-          expose = no_report_elements))
-    }
+    try { XML.content(clean_output(YXML.parse_body(YXML.Source(msg)))) }
     catch { case ERROR(_) => msg }
 }