# HG changeset patch
# User wenzelm
# Date 1348866159 -7200
# Node ID c7585f8addc225712c0fb882ff505d95cd997c10
# Parent  9fad6480300deb81edbacc911f4fc58f467608f2
tuned;

diff -r 9fad6480300d -r c7585f8addc2 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Fri Sep 28 22:53:18 2012 +0200
+++ b/src/Pure/General/pretty.scala	Fri Sep 28 23:02:39 2012 +0200
@@ -97,11 +97,7 @@
     val emergencypos = margin / 2
 
     def content_length(tree: XML.Tree): Double =
-      tree match {
-        case XML.Wrapped_Elem(_, _, body) => (0.0 /: body)(_ + content_length(_))
-        case XML.Elem(_, body) => (0.0 /: body)(_ + content_length(_))
-        case XML.Text(s) => metric(s)
-      }
+      XML.traverse_text(List(tree))(0.0)(_ + metric(_))
 
     def breakdist(trees: XML.Body, after: Double): Double =
       trees match {