--- a/src/Pure/General/pretty.scala Sat Dec 19 22:25:01 2015 +0100
+++ b/src/Pure/General/pretty.scala Sat Dec 19 23:16:47 2015 +0100
@@ -9,13 +9,23 @@
object Pretty
{
- /* spaces */
+ /* XML constructors */
+
+ def spaces(n: Int): XML.Body = if (n == 0) Nil else List(XML.Text(Symbol.spaces(n)))
+ val space: XML.Body = spaces(1)
- def spaces(n: Int): XML.Body =
- if (n == 0) Nil
- else List(XML.Text(Symbol.spaces(n)))
+ def block(consistent: Boolean, indent: Int, body: XML.Body): XML.Tree =
+ XML.Elem(Markup.Block(consistent, indent), body)
+ def block(indent: Int, body: XML.Body): XML.Tree = block(false, indent, body)
+ def block(body: XML.Body): XML.Tree = block(2, body)
- val space: XML.Body = spaces(1)
+ def brk(width: Int, indent: Int = 0): XML.Tree =
+ XML.Elem(Markup.Break(width, indent), spaces(width))
+
+ val fbrk: XML.Tree = XML.Text("\n")
+
+ val Separator: XML.Body = List(XML.elem(Markup.SEPARATOR, space), fbrk)
+ def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
/* text metric -- standardized to width of space */
@@ -24,8 +34,6 @@
{
val unit: Double
def apply(s: String): Double
- def content_length(body: XML.Body): Double =
- XML.traverse_text(body)(0.0)(_ + apply(_))
}
object Metric_Default extends Metric
@@ -37,51 +45,41 @@
/* markup trees with physical blocks and breaks */
- def block(body: XML.Body): XML.Tree = Block(false, 2, body)
-
- object Block
- {
- def apply(consistent: Boolean, indent: Int, body: XML.Body): XML.Tree =
- XML.Elem(Markup.Block(consistent, indent), body)
+ sealed abstract class Tree { def length: Double }
+ case class Block(
+ markup: Option[(Markup, Option[XML.Body])],
+ consistent: Boolean, indent: Int, body: List[Tree], length: Double) extends Tree
+ case class Str(string: String, length: Double) extends Tree
+ case class Break(force: Boolean, width: Int, indent: Int) extends Tree
+ { def length: Double = width.toDouble }
- def unapply(tree: XML.Tree): Option[(Boolean, Int, XML.Body)] =
- tree match {
- case XML.Elem(Markup.Block(consistent, indent), body) => Some((consistent, indent, body))
- case _ => None
- }
- }
+ val FBreak = Break(true, 1, 0)
- object Break
- {
- def apply(w: Int, i: Int = 0): XML.Tree =
- XML.Elem(Markup.Break(w, i), spaces(w))
+ def make_block(
+ markup: Option[(Markup, Option[XML.Body])],
+ consistent: Boolean,
+ indent: Int,
+ body: List[Tree]): Tree =
+ Block(markup, consistent, indent, body, (0.0 /: body) { case (n, t) => n + t.length })
- def unapply(tree: XML.Tree): Option[(Int, Int)] =
- tree match {
- case XML.Elem(Markup.Break(w, i), _) => Some((w, i))
- case _ => None
- }
- }
-
- val FBreak = XML.Text("\n")
-
- def item(body: XML.Body): XML.Tree =
- Block(false, 2, XML.elem(Markup.BULLET, space) :: space ::: body)
-
- val Separator = List(XML.elem(Markup.SEPARATOR, space), FBreak)
- def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
-
-
- /* standard form */
-
- def standard_form(body: XML.Body): XML.Body =
- body flatMap {
+ def make_tree(metric: Metric, xml: XML.Body): List[Tree] =
+ xml flatMap {
case XML.Wrapped_Elem(markup, body1, body2) =>
- List(XML.Wrapped_Elem(markup, body1, standard_form(body2)))
+ List(make_block(Some(markup, Some(body1)), false, 0, make_tree(metric, body2)))
case XML.Elem(markup, body) =>
- if (markup.name == Markup.ITEM) List(item(standard_form(body)))
- else List(XML.Elem(markup, standard_form(body)))
- case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
+ markup match {
+ case Markup.Block(consistent, indent) =>
+ List(make_block(None, consistent, indent, make_tree(metric, body)))
+ case Markup.Break(width, indent) =>
+ List(Break(false, width, indent))
+ case Markup(Markup.ITEM, _) =>
+ List(make_block(None, false, 2,
+ make_tree(metric, XML.elem(Markup.BULLET, space) :: space ::: body)))
+ case _ =>
+ List(make_block(Some((markup, None)), false, 0, make_tree(metric, body)))
+ }
+ case XML.Text(text) =>
+ Library.separate(FBreak, split_lines(text).map(s => Str(s, metric(s))))
}
@@ -94,76 +92,68 @@
{
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 =
- if (s == "") this
- else copy(tx = XML.Text(s) :: tx, pos = pos + metric(s))
- def blanks(wd: Int): Text = string(Symbol.spaces(wd))
+ def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1)
+ def string(s: String, len: Double): Text =
+ copy(tx = if (s == "") tx else XML.Text(s) :: tx, pos = pos + len)
+ def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
def content: XML.Body = tx.reverse
}
val breakgain = margin / 20
val emergencypos = (margin / 2).round.toInt
- def break_dist(trees: XML.Body, after: Double): Double =
+ def break_dist(trees: List[Tree], after: Double): Double =
trees match {
- case Break(_, _) :: _ => 0.0
- case FBreak :: _ => 0.0
- case t :: ts => metric.content_length(List(t)) + break_dist(ts, after)
+ case (_: Break) :: _ => 0.0
+ case t :: ts => t.length + break_dist(ts, after)
case Nil => after
}
- def force_all(trees: XML.Body): XML.Body =
- trees flatMap {
- case Break(_, ind) => FBreak :: spaces(ind)
- case tree => List(tree)
- }
+ def force_break(tree: Tree): Tree =
+ tree match { case Break(false, wd, ind) => Break(true, wd, ind) case _ => tree }
+ def force_all(trees: List[Tree]): List[Tree] = trees.map(force_break(_))
- def force_next(trees: XML.Body): XML.Body =
+ def force_next(trees: List[Tree]): List[Tree] =
trees match {
case Nil => Nil
- case FBreak :: _ => trees
- case Break(_, ind) :: ts => FBreak :: spaces(ind) ::: ts
+ case (t: Break) :: ts => force_break(t) :: ts
case t :: ts => t :: force_next(ts)
}
- def format(trees: XML.Body, blockin: Int, after: Double, text: Text): Text =
+ def format(trees: List[Tree], blockin: Int, after: Double, text: Text): Text =
trees match {
case Nil => text
- case Block(consistent, indent, body) :: ts =>
+ case Block(markup, consistent, indent, body, blen) :: ts =>
val pos1 = (text.pos + indent).ceil.toInt
val pos2 = pos1 % emergencypos
val blockin1 = if (pos1 < emergencypos) pos1 else pos2
- val blen = metric.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 btext =
+ markup match {
+ case None => format(body1, blockin1, d, text)
+ case Some((m, markup_body)) =>
+ val btext0 = format(body1, blockin1, d, text.copy(tx = Nil))
+ val elem =
+ markup_body match {
+ case None => XML.Elem(m, btext0.content)
+ case Some(b) => XML.Wrapped_Elem(m, b, btext0.content)
+ }
+ btext0.copy(tx = elem :: text.tx)
+ }
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 - break_dist(ts, after)) max (blockin + breakgain)))
+ case Break(force, wd, ind) :: ts =>
+ if (!force &&
+ 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, 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, 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)
-
- case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
+ case Str(s, len) :: ts => format(ts, blockin, after, text.string(s, len))
}
-
- format(standard_form(input), 0, 0.0, Text()).content
+ format(make_tree(metric, input), 0, 0.0, Text()).content
}
def string_of(input: XML.Body, margin: Double = margin_default,
@@ -177,15 +167,17 @@
{
def fmt(tree: XML.Tree): XML.Body =
tree match {
- case Block(_, _, body) => body.flatMap(fmt)
- case Break(wd, _) => spaces(wd)
- case FBreak => space
case XML.Wrapped_Elem(markup, body1, body2) =>
List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt)))
- case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
- case XML.Text(_) => List(tree)
+ case XML.Elem(markup, body) =>
+ markup match {
+ case Markup.Block(_, _) => body.flatMap(fmt)
+ case Markup.Break(wd, _) => spaces(wd)
+ case _ => List(XML.Elem(markup, body.flatMap(fmt)))
+ }
+ case XML.Text(s) => List(XML.Text(s.replace('\n', ' ')))
}
- standard_form(input).flatMap(fmt)
+ input.flatMap(fmt)
}
def str_of(input: XML.Body): String = XML.content(unformatted(input))