# HG changeset patch
# User wenzelm
# Date 1273264048 -7200
# Node ID 93753a8c955081a0575f61481c702534825c5857
# Parent  42b7f881f5fc12d4f161c2afca899c0f4873381c
unformatted output;

diff -r 42b7f881f5fc -r 93753a8c9550 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Fri May 07 22:00:23 2010 +0200
+++ b/src/Pure/General/pretty.scala	Fri May 07 22:27:28 2010 +0200
@@ -115,6 +115,25 @@
     format(input.flatMap(standard_format), 0, 0, Text()).content
   }
 
-  def string_of(trees: List[XML.Tree], margin: Int = default_margin): String =
-    formatted(trees).iterator.flatMap(XML.content).mkString
+  def string_of(input: List[XML.Tree], margin: Int = default_margin): String =
+    formatted(input).iterator.flatMap(XML.content).mkString
+
+
+  /* unformatted output */
+
+  def unformatted(input: List[XML.Tree]): List[XML.Tree] =
+  {
+    def fmt(tree: XML.Tree): List[XML.Tree] =
+      tree match {
+        case Block(_, body) => body.flatMap(fmt)
+        case Break(wd) => List(XML.Text(" " * wd))
+        case FBreak => List(XML.Text(" "))
+        case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(fmt)))
+        case XML.Text(_) => List(tree)
+      }
+    input.flatMap(standard_format).flatMap(fmt)
+  }
+
+  def str_of(input: List[XML.Tree]): String =
+    unformatted(input).iterator.flatMap(XML.content).mkString
 }