src/Pure/General/pretty.scala
changeset 51569 4e084727faae
parent 51568 cdb4b7dc76cb
child 51570 3633828d80fc
equal deleted inserted replaced
51568:cdb4b7dc76cb 51569:4e084727faae
    99       def blanks(wd: Int): Text = string(spaces(wd))
    99       def blanks(wd: Int): Text = string(spaces(wd))
   100       def content: XML.Body = tx.reverse
   100       def content: XML.Body = tx.reverse
   101     }
   101     }
   102 
   102 
   103     val breakgain = margin / 20
   103     val breakgain = margin / 20
   104     val emergencypos = margin / 2
   104     val emergencypos = (margin / 2).round.toInt
   105 
   105 
   106     def content_length(tree: XML.Tree): Double =
   106     def content_length(tree: XML.Tree): Double =
   107       XML.traverse_text(List(tree))(0.0)(_ + metric(_))
   107       XML.traverse_text(List(tree))(0.0)(_ + metric(_))
   108 
   108 
   109     def breakdist(trees: XML.Body, after: Double): Double =
   109     def breakdist(trees: XML.Body, after: Double): Double =
   120         case FBreak :: _ => trees
   120         case FBreak :: _ => trees
   121         case Break(_) :: ts => FBreak :: ts
   121         case Break(_) :: ts => FBreak :: ts
   122         case t :: ts => t :: forcenext(ts)
   122         case t :: ts => t :: forcenext(ts)
   123       }
   123       }
   124 
   124 
   125     def format(trees: XML.Body, blockin: Double, after: Double, text: Text): Text =
   125     def format(trees: XML.Body, blockin: Int, after: Double, text: Text): Text =
   126       trees match {
   126       trees match {
   127         case Nil => text
   127         case Nil => text
   128 
   128 
   129         case Block(indent, body) :: ts =>
   129         case Block(indent, body) :: ts =>
   130           val pos1 = text.pos + indent
   130           val pos1 = (text.pos + indent).ceil.toInt
   131           val pos2 = pos1 % emergencypos
   131           val pos2 = pos1 % emergencypos
   132           val blockin1 =
   132           val blockin1 =
   133             if (pos1 < emergencypos) pos1
   133             if (pos1 < emergencypos) pos1
   134             else pos2
   134             else pos2
   135           val btext = format(body, blockin1, breakdist(ts, after), text)
   135           val btext = format(body, blockin1, breakdist(ts, after), text)
   137           format(ts1, blockin, after, btext)
   137           format(ts1, blockin, after, btext)
   138 
   138 
   139         case Break(wd) :: ts =>
   139         case Break(wd) :: ts =>
   140           if (text.pos + wd <= ((margin - breakdist(ts, after)) max (blockin + breakgain)))
   140           if (text.pos + wd <= ((margin - breakdist(ts, after)) max (blockin + breakgain)))
   141             format(ts, blockin, after, text.blanks(wd))
   141             format(ts, blockin, after, text.blanks(wd))
   142           else format(ts, blockin, after, text.newline.blanks(blockin.toInt))
   142           else format(ts, blockin, after, text.newline.blanks(blockin))
   143         case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt))
   143         case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
   144 
   144 
   145         case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
   145         case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
   146           val btext = format(body2, blockin, breakdist(ts, after), text.copy(tx = Nil))
   146           val btext = format(body2, blockin, breakdist(ts, after), text.copy(tx = Nil))
   147           val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
   147           val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
   148           val btext1 = btext.copy(tx = XML.Wrapped_Elem(markup, body1, btext.content) :: text.tx)
   148           val btext1 = btext.copy(tx = XML.Wrapped_Elem(markup, body1, btext.content) :: text.tx)
   155           format(ts1, blockin, after, btext1)
   155           format(ts1, blockin, after, btext1)
   156 
   156 
   157         case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
   157         case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
   158       }
   158       }
   159 
   159 
   160     format(standard_format(input), 0.0, 0.0, Text()).content
   160     format(standard_format(input), 0, 0.0, Text()).content
   161   }
   161   }
   162 
   162 
   163   def string_of(input: XML.Body, margin: Double = margin_default,
   163   def string_of(input: XML.Body, margin: Double = margin_default,
   164       metric: Metric = Metric_Default): String =
   164       metric: Metric = Metric_Default): String =
   165     XML.content(formatted(input, margin, metric))
   165     XML.content(formatted(input, margin, metric))