# HG changeset patch
# User wenzelm
# Date 1273656532 -7200
# Node ID 599466689412a7f20cd1551ae29f5809d7f48173
# Parent  ed97e877ff2d920a055a71a48e2b93f06a085f80
tuned;

diff -r ed97e877ff2d -r 599466689412 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Tue May 11 23:36:06 2010 +0200
+++ b/src/Pure/General/pretty.scala	Wed May 12 11:28:52 2010 +0200
@@ -62,9 +62,10 @@
   }
 
   private val margin_default = 76
+  private def metric_default(s: String) = s.length.toDouble
 
   def formatted(input: List[XML.Tree], margin: Int = margin_default,
-    metric: String => Double = (_.length.toDouble)): List[XML.Tree] =
+    metric: String => Double = metric_default): List[XML.Tree] =
   {
     val breakgain = margin / 20
     val emergencypos = margin / 2
@@ -79,9 +80,7 @@
       trees match {
         case Break(_) :: _ => 0.0
         case FBreak :: _ => 0.0
-        case XML.Elem(_, _, body) :: ts =>
-          (0.0 /: body)(_ + content_length(_)) + breakdist(ts, after)
-        case XML.Text(s) :: ts => metric(s) + breakdist(ts, after)
+        case t :: ts => content_length(t) + breakdist(ts, after)
         case Nil => after
       }
 
@@ -123,7 +122,8 @@
     format(input.flatMap(standard_format), 0.0, 0.0, Text()).content
   }
 
-  def string_of(input: List[XML.Tree], margin: Int = margin_default): String =
+  def string_of(input: List[XML.Tree], margin: Int = margin_default,
+      metric: String => Double = metric_default): String =
     formatted(input).iterator.flatMap(XML.content).mkString