diff -r 84f1951bcc3c -r 75886eea238a src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Sun Dec 29 15:58:47 2024 +0100 +++ b/src/Pure/General/pretty.scala Mon Dec 30 14:39:33 2024 +0100 @@ -60,21 +60,28 @@ private def force_nat(i: Int): Int = i max 0 + type Markup_Body = (Markup, Option[XML.Body]) + val no_markup: Markup_Body = (Markup.Empty, None) + val item_markup: Markup_Body = (Markup.Expression.item, None) + + def markup_elem(markup: Markup_Body, body: XML.Body): XML.Elem = + markup match { + case (m, None) => XML.Elem(m, body) + case (m1, Some(m2)) => XML.Wrapped_Elem(m1, m2, body) + } + private sealed abstract class Tree { def length: Double } + private case object End extends Tree { + override def length: Double = 0.0 + } private case class Block( - markup: Markup, - markup_body: Option[XML.Body], + markup: Markup_Body, open_block: Boolean, consistent: Boolean, indent: Int, body: List[Tree], length: Double - ) extends Tree { - def no_markup: Boolean = markup.is_empty && markup_body.isEmpty - def markup_elem(body: XML.Body): XML.Elem = - if (markup_body.isEmpty) XML.Elem(markup, body) - else XML.Wrapped_Elem(markup, markup_body.get, body) - } + ) extends Tree private case class Break(force: Boolean, width: Int, indent: Int) extends Tree { def length: Double = width.toDouble } @@ -83,8 +90,7 @@ private val FBreak = Break(true, 1, 0) private def make_block(body: List[Tree], - markup: Markup = Markup.Empty, - markup_body: Option[XML.Body] = None, + markup: Markup_Body = no_markup, open_block: Boolean = false, consistent: Boolean = false, indent: Int = 0 @@ -101,7 +107,7 @@ case Nil => len1 } } - Block(markup, markup_body, open_block, consistent, indent1, body, body_length(body, 0.0)) + Block(markup, open_block, consistent, indent1, body, body_length(body, 0.0)) } @@ -125,14 +131,42 @@ /* formatting */ - private sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0) { - def set(body: XML.Body): Text = copy(tx = body) - def reset: Text = if (tx.isEmpty) this else copy(tx = Nil) - def content: XML.Body = tx.reverse + private type State = List[(Markup_Body, List[XML.Tree])] + private val init_state: State = List((no_markup, Nil)) + + private sealed case class Text( + state: State = init_state, + pos: Double = 0.0, + nl: Int = 0 + ) { + def add(t: XML.Tree, len: Double = 0.0): Text = + (state: @unchecked) match { + case (m, ts) :: rest => copy(state = (m, t :: ts) :: rest, pos = pos + len) + } + + def push(m: Markup_Body): Text = + copy(state = (m, Nil) :: state) - def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1) + def pop: Text = + (state: @unchecked) match { + case (m1, ts1) :: (m2, ts2) :: rest => + copy(state = (m2, markup_elem(m1, ts1.reverse) :: ts2) :: rest) + } + + def result: XML.Body = + (state: @unchecked) match { + case List((m, ts)) if m == no_markup => ts.reverse + } + + def reset: Text = copy(state = init_state) + def restore(other: Text): Text = copy(state = other.state) + + def newline: Text = add(fbrk).copy(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) + if (s.isEmpty) copy(pos = pos + len) + else add(XML.Text(s), len = len) + def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble) } @@ -166,9 +200,8 @@ def make_tree(inp: XML.Body): List[Tree] = inp flatMap { - case XML.Wrapped_Elem(markup, markup_body, body) => - List(make_block(make_tree(body), - markup = markup, markup_body = Some(markup_body), open_block = true)) + case XML.Wrapped_Elem(markup1, markup2, body) => + List(make_block(make_tree(body), markup = (markup1, Some(markup2)), open_block = true)) case XML.Elem(markup, body) => markup match { case Markup.Block(consistent, indent) => @@ -176,10 +209,9 @@ case Markup.Break(width, indent) => List(Break(false, force_nat(width), force_nat(indent))) case Markup(Markup.ITEM, _) => - val item = make_tree(bullet ::: body) - List(make_block(item, markup = Markup.Expression.item, indent = 2)) + List(make_block(make_tree(bullet ::: body), markup = item_markup, indent = 2)) case _ => - List(make_block(make_tree(body), markup = markup, open_block = true)) + List(make_block(make_tree(body), markup = (markup, None), open_block = true)) } case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(s => Str(s, metric(s)))) @@ -189,12 +221,11 @@ trees match { case Nil => text + case End :: ts => + format(ts, blockin, after, text.pop) + case (block: Block) :: ts if block.open_block => - val btext = format(block.body, blockin, break_dist(ts, after), text.reset) - val elem = block.markup_elem(btext.content) - val btext1 = btext.set(elem :: text.tx) - val ts1 = if (text.nl < btext1.nl) force_next(ts) else ts - format(ts1, blockin, after, btext1) + format(block.body ::: End :: ts, blockin, after, text.push(block.markup)) case (block: Block) :: ts => val pos1 = (text.pos + block.indent).ceil.toInt @@ -205,11 +236,11 @@ if (block.consistent && text.pos + block.length > margin - after1) force_all(block.body) else block.body val btext1 = - if (block.no_markup) format(body1, blockin1, after1, text) + if (block.markup == no_markup) format(body1, blockin1, after1, text) else { val btext = format(body1, blockin1, after1, text.reset) - val elem = block.markup_elem(btext.content) - btext.set(elem :: text.tx) + val elem = markup_elem(block.markup, btext.result) + btext.restore(text.add(elem)) } val ts1 = if (text.nl < btext1.nl) force_next(ts) else ts format(ts1, blockin, after, btext1) @@ -222,7 +253,7 @@ case Str(s, len) :: ts => format(ts, blockin, after, text.string(s, len)) } - format(make_tree(input), 0, 0.0, Text()).content + format(make_tree(input), 0, 0.0, Text()).result } def string_of(input: XML.Body,