# HG changeset patch
# User wenzelm
# Date 1450612248 -3600
# Node ID 5348b76aa94cc75750531837757b08f7216cef06
# Parent  a942e237c9e8a79ff2cc05cf19957e656a01ddf3
unused;

diff -r a942e237c9e8 -r 5348b76aa94c src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sun Dec 20 12:48:56 2015 +0100
+++ b/src/Pure/General/pretty.scala	Sun Dec 20 12:50:48 2015 +0100
@@ -162,26 +162,4 @@
   def string_of(input: XML.Body, margin: Double = margin_default,
       metric: Metric = Metric_Default): String =
     XML.content(formatted(input, margin, metric))
-
-
-  /* unformatted output */
-
-  def unformatted(input: XML.Body): XML.Body =
-  {
-    def fmt(tree: XML.Tree): XML.Body =
-      tree match {
-        case XML.Wrapped_Elem(markup, body1, body2) =>
-          List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt)))
-        case XML.Elem(markup, body) =>
-          markup match {
-            case Markup.Block(_, _) => body.flatMap(fmt)
-            case Markup.Break(wd, _) => spaces(wd)
-            case _ => List(XML.Elem(markup, body.flatMap(fmt)))
-          }
-        case XML.Text(s) => List(XML.Text(s.replace('\n', ' ')))
-      }
-    input.flatMap(fmt)
-  }
-
-  def str_of(input: XML.Body): String = XML.content(unformatted(input))
 }