--- a/src/Pure/General/pretty.scala Sat Dec 19 10:59:14 2015 +0100
+++ b/src/Pure/General/pretty.scala Sat Dec 19 14:47:52 2015 +0100
@@ -22,6 +22,10 @@
else space * k
}
+ def spaces_body(k: Int): XML.Body =
+ if (k == 0) Nil
+ else List(XML.Text(spaces(k)))
+
/* text metric -- standardized to width of space */
@@ -40,16 +44,16 @@
/* markup trees with physical blocks and breaks */
- def block(body: XML.Body): XML.Tree = Block(2, body)
+ def block(body: XML.Body): XML.Tree = Block(false, 2, body)
object Block
{
- def apply(i: Int, body: XML.Body): XML.Tree =
- XML.Elem(Markup.Block(i), body)
+ def apply(consistent: Boolean, indent: Int, body: XML.Body): XML.Tree =
+ XML.Elem(Markup.Block(consistent, indent), body)
- def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
+ def unapply(tree: XML.Tree): Option[(Boolean, Int, XML.Body)] =
tree match {
- case XML.Elem(Markup.Block(i), body) => Some((i, body))
+ case XML.Elem(Markup.Block(consistent, indent), body) => Some((consistent, indent, body))
case _ => None
}
}
@@ -57,7 +61,7 @@
object Break
{
def apply(w: Int, i: Int = 0): XML.Tree =
- XML.Elem(Markup.Break(w, i), List(XML.Text(spaces(w))))
+ XML.Elem(Markup.Break(w, i), spaces_body(w))
def unapply(tree: XML.Tree): Option[(Int, Int)] =
tree match {
@@ -69,7 +73,7 @@
val FBreak = XML.Text("\n")
def item(body: XML.Body): XML.Tree =
- Block(2, XML.elem(Markup.BULLET, List(XML.Text(space))) :: XML.Text(space) :: body)
+ Block(false, 2, XML.elem(Markup.BULLET, List(XML.Text(space))) :: XML.Text(space) :: body)
val Separator = List(XML.elem(Markup.SEPARATOR, List(XML.Text(space))), FBreak)
def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
@@ -98,7 +102,9 @@
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))
+ def string(s: String): Text =
+ if (s == "") this
+ else copy(tx = XML.Text(s) :: tx, pos = pos + metric(s))
def blanks(wd: Int): Text = string(spaces(wd))
def content: XML.Body = tx.reverse
}
@@ -106,54 +112,63 @@
val breakgain = margin / 20
val emergencypos = (margin / 2).round.toInt
- def content_length(tree: XML.Tree): Double =
- XML.traverse_text(List(tree))(0.0)(_ + metric(_))
+ def content_length(body: XML.Body): Double =
+ XML.traverse_text(body)(0.0)(_ + metric(_))
- def breakdist(trees: XML.Body, after: Double): Double =
+ def break_dist(trees: XML.Body, after: Double): Double =
trees match {
case Break(_, _) :: _ => 0.0
case FBreak :: _ => 0.0
- case t :: ts => content_length(t) + breakdist(ts, after)
+ case t :: ts => content_length(List(t)) + break_dist(ts, after)
case Nil => after
}
- def forcenext(trees: XML.Body): XML.Body =
+ def force_all(trees: XML.Body): XML.Body =
+ trees flatMap {
+ case Break(_, ind) => FBreak :: spaces_body(ind)
+ case tree => List(tree)
+ }
+
+ def force_next(trees: XML.Body): XML.Body =
trees match {
case Nil => Nil
case FBreak :: _ => trees
- case Break(_, _) :: ts => FBreak :: ts
- case t :: ts => t :: forcenext(ts)
+ case Break(_, ind) :: ts => FBreak :: spaces_body(ind) ::: ts
+ case t :: ts => t :: force_next(ts)
}
def format(trees: XML.Body, blockin: Int, after: Double, text: Text): Text =
trees match {
case Nil => text
- case Block(indent, body) :: ts =>
+ case Block(consistent, indent, body) :: ts =>
val pos1 = (text.pos + indent).ceil.toInt
val pos2 = pos1 % emergencypos
val blockin1 =
if (pos1 < emergencypos) pos1
else pos2
- val btext = format(body, blockin1, breakdist(ts, after), text)
- val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
+ val blen = content_length(body)
+ val d = break_dist(ts, after)
+ val body1 = if (consistent && text.pos + blen > margin - d) force_all(body) else body
+ val btext = format(body1, blockin1, d, text)
+ val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
format(ts1, blockin, after, btext)
case Break(wd, ind) :: ts =>
- if (text.pos + wd <= ((margin - breakdist(ts, after)) max (blockin + breakgain)))
+ if (text.pos + wd <= ((margin - break_dist(ts, after)) max (blockin + breakgain)))
format(ts, blockin, after, text.blanks(wd))
else format(ts, blockin, after, text.newline.blanks(blockin + ind))
case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
- val btext = format(body2, blockin, breakdist(ts, after), text.copy(tx = Nil))
- val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
+ val btext = format(body2, blockin, break_dist(ts, after), text.copy(tx = Nil))
+ val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
val btext1 = btext.copy(tx = XML.Wrapped_Elem(markup, body1, btext.content) :: text.tx)
format(ts1, blockin, after, btext1)
case XML.Elem(markup, body) :: ts =>
- val btext = format(body, blockin, breakdist(ts, after), text.copy(tx = Nil))
- val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
+ val btext = format(body, blockin, break_dist(ts, after), text.copy(tx = Nil))
+ val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx)
format(ts1, blockin, after, btext1)
@@ -174,8 +189,8 @@
{
def fmt(tree: XML.Tree): XML.Body =
tree match {
- case Block(_, body) => body.flatMap(fmt)
- case Break(wd, _) => List(XML.Text(spaces(wd)))
+ case Block(_, _, body) => body.flatMap(fmt)
+ case Break(wd, _) => spaces_body(wd)
case FBreak => List(XML.Text(space))
case XML.Wrapped_Elem(markup, body1, body2) =>
List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt)))