diff -r 25b7e843e124 -r 8b06b99fb85c src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Thu Sep 20 13:34:27 2012 +0200
+++ b/src/Pure/General/pretty.scala	Thu Sep 20 15:00:14 2012 +0200
@@ -62,9 +62,9 @@
 
   /* formatted output */
 
-  private def standard_format(tree: XML.Tree): XML.Body =
-    tree match {
-      case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(standard_format)))
+  def standard_format(body: XML.Body): XML.Body =
+    body flatMap {
+      case XML.Elem(markup, body) => List(XML.Elem(markup, standard_format(body)))
       case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
     }
 
@@ -141,7 +141,7 @@
           format(ts1, blockin, after, btext1)
         case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s, metric(s)))
       }
-    format(input.flatMap(standard_format), 0.0, 0.0, Text()).content
+    format(standard_format(input), 0.0, 0.0, Text()).content
   }
 
   def string_of(input: XML.Body, margin: Int = margin_default,
@@ -161,7 +161,7 @@
         case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
         case XML.Text(_) => List(tree)
       }
-    input.flatMap(standard_format).flatMap(fmt)
+    standard_format(input).flatMap(fmt)
   }
 
   def str_of(input: XML.Body): String = XML.content(unformatted(input))