# HG changeset patch
# User wenzelm
# Date 1364478457 -3600
# Node ID cdb4b7dc76cbec4caa602a55d12b207ec9c62926
# Parent  a86c5e02ba58095ceeb0961227294b46dab5b8e6
tuned;

diff -r a86c5e02ba58 -r cdb4b7dc76cb src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Thu Mar 28 14:01:56 2013 +0100
+++ b/src/Pure/General/pretty.scala	Thu Mar 28 14:47:37 2013 +0100
@@ -92,7 +92,7 @@
   def formatted(input: XML.Body, margin: Double = margin_default,
     metric: Metric = Metric_Default): XML.Body =
   {
-    sealed case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
+    sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
     {
       def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
       def string(s: String): Text = copy(tx = XML.Text(s) :: tx, pos = pos + metric(s))
@@ -137,7 +137,7 @@
           format(ts1, blockin, after, btext)
 
         case Break(wd) :: ts =>
-          if (text.pos + wd <= (margin - breakdist(ts, after)).max(blockin + breakgain))
+          if (text.pos + wd <= ((margin - breakdist(ts, after)) max (blockin + breakgain)))
             format(ts, blockin, after, text.blanks(wd))
           else format(ts, blockin, after, text.newline.blanks(blockin.toInt))
         case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt))