# HG changeset patch
# User wenzelm
# Date 1662646964 -7200
# Node ID 338adf8d423cb512b7679636a88d2ed871009093
# Parent  3f5028b5441914d6422b235399f51222d305054b
support Pretty.unformatted, similar to ML version;

diff -r 3f5028b54419 -r 338adf8d423c src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Thu Sep 08 13:16:46 2022 +0200
+++ b/src/Pure/General/pretty.scala	Thu Sep 08 16:22:44 2022 +0200
@@ -92,6 +92,23 @@
   }
 
 
+  /* unformatted output */
+
+  def unformatted(input: XML.Body): XML.Body = {
+    input flatMap {
+      case XML.Wrapped_Elem(markup, body1, body2) =>
+        List(XML.Wrapped_Elem(markup, body1, unformatted(body2)))
+      case XML.Elem(markup, body) =>
+        markup match {
+          case Markup.Block(_, _) => unformatted(body)
+          case Markup.Break(width, _) => XML.string(Symbol.spaces(width))
+          case _ => List(XML.Elem(markup, unformatted(body)))
+        }
+      case XML.Text(text) => XML.string(split_lines(text).mkString(Symbol.space))
+    }
+  }
+
+
   /* formatted output */
 
   private sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0) {