src/Pure/General/pretty.scala

   }
 
 
   /* 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) =>
         List(XML.Wrapped_Elem(markup, body1, unbreakable(body2)))
       case XML.Elem(Markup.Break(width, _), _) => spaces(width)
       case XML.Elem(markup, body) => List(XML.Elem(markup, unbreakable(body)))
       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 */
 
   private sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0) {

       }
     format(make_tree(input), 0, 0.0, Text()).content
   }
 
   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))
+  }
 }