# HG changeset patch # User wenzelm # Date 1735654176 -3600 # Node ID 1629c2ff4880da0a7c03de414f143c868f7a76c7 # Parent b540572e3fd24545ea1953cd38f4063eacddca56 misc tuning: more uniform; diff -r b540572e3fd2 -r 1629c2ff4880 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Mon Dec 30 21:36:58 2024 +0100 +++ b/src/Pure/General/pretty.ML Tue Dec 31 15:09:36 2024 +0100 @@ -378,6 +378,8 @@ | force_next ((prt as Break _) :: prts) = force_break prt :: prts | force_next (prt :: prts) = prt :: force_next prts; +nonfix before; + in fun format_tree (ops: output_ops) input = @@ -406,39 +408,41 @@ val ind' = Buffer.add s Buffer.empty; in {markups = markups, tx = tx', ind = ind', pos = n, nl = nl + 1} end; - (*blockin is the indentation of the current block; - after is the width of the following context until next break.*) - fun format ([], _, _) text = text - | format (prt :: prts, block as (_, blockin), after) (text as {ind, pos, nl, ...}) = - (case prt of - End => format (prts, block, after) (pop text) - | Block {markup, open_block = true, body, ...} => - text |> push markup |> format (body @ End :: prts, block, after) - | Block {markup, consistent, indent, body, length = blen, ...} => - let - val pos' = pos + indent; - val pos'' = pos' mod emergencypos; - val block' = - if pos' < emergencypos - then (add_indent indent ind, pos') - else (add_indent pos'' Buffer.empty, pos''); - val after' = break_dist (prts, after) - val body' = body - |> (consistent andalso pos + blen > margin - after') ? map force_break; - val btext: text = - text |> push markup |> format (body' @ [End], block', after'); - (*if this block was broken then force the next break*) - val prts' = if nl < #nl btext then force_next prts else prts; - in format (prts', block, after) btext end - | Break (force, wd, ind) => - (*no break if text to next break fits on this line - or if breaking would add only breakgain to space*) - format (prts, block, after) - (if not force andalso - pos + wd <= Int.max (margin - break_dist (prts, after), blockin + breakgain) - then text |> blanks wd (*just insert wd blanks*) - else text |> break_indent block |> blanks ind) - | Str str => format (prts, block, after) (string str text)); + nonfix before; + + (*'before' is the indentation context of the current block*) + (*'after' is the width of the input context until the next break*) + fun format (trees, before, after) (text as {pos, ...}) = + (case trees of + [] => text + | End :: ts => format (ts, before, after) (pop text) + | Block {markup, open_block = true, body, ...} :: ts => + text |> push markup |> format (body @ End :: ts, before, after) + | Block {markup, consistent, indent, body, length = blen, ...} :: ts => + let + val pos' = pos + indent; + val pos'' = pos' mod emergencypos; + val before' = + if pos' < emergencypos + then (add_indent indent (#ind text), pos') + else (add_indent pos'' Buffer.empty, pos''); + val after' = break_dist (ts, after) + val body' = body + |> (consistent andalso pos + blen > margin - after') ? map force_break; + val btext: text = + text |> push markup |> format (body' @ [End], before', after'); + (*if this block was broken then force the next break*) + val ts' = if #nl text < #nl btext then force_next ts else ts; + in format (ts', before, after) btext end + | Break (force, wd, ind) :: ts => + (*no break if text to next break fits on this line + or if breaking would add only breakgain to space*) + format (ts, before, after) + (if not force andalso + pos + wd <= Int.max (margin - break_dist (ts, after), #2 before + breakgain) + then text |> blanks wd (*just insert wd blanks*) + else text |> break_indent before |> blanks ind) + | Str str :: ts => format (ts, before, after) (string str text)); in #tx (format ([output_tree ops true input], (Buffer.empty, 0), 0) empty) end; diff -r b540572e3fd2 -r 1629c2ff4880 src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Mon Dec 30 21:36:58 2024 +0100 +++ b/src/Pure/General/pretty.scala Tue Dec 31 15:09:36 2024 +0100 @@ -217,41 +217,35 @@ Library.separate(FBreak, split_lines(text).map(s => Str(s, metric(s)))) } - def format(trees: List[Tree], blockin: Int, after: Double, text: Text): Text = + def format(trees: List[Tree], before: Int, after: Double, text: Text): Text = trees match { case Nil => text - - case End :: ts => - format(ts, blockin, after, text.pop) - + case End :: ts => format(ts, before, after, text.pop) case (block: Block) :: ts if block.open_block => - format(block.body ::: End :: ts, blockin, after, text.push(block.markup)) - + format(block.body ::: End :: ts, before, after, text.push(block.markup)) case (block: Block) :: ts => val pos1 = (text.pos + block.indent).ceil.toInt val pos2 = pos1 % emergencypos - val blockin1 = if (pos1 < emergencypos) pos1 else pos2 + val before1 = if (pos1 < emergencypos) pos1 else pos2 val after1 = break_dist(ts, after) val body1 = if (block.consistent && text.pos + block.length > margin - after1) force_all(block.body) else block.body val btext1 = - if (block.markup == no_markup) format(body1, blockin1, after1, text) + if (block.markup == no_markup) format(body1, before1, after1, text) else { - val btext = format(body1, blockin1, after1, text.reset) + val btext = format(body1, before1, after1, text.reset) 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) - + format(ts1, before, after, btext1) 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 Str(s, len) :: ts => format(ts, blockin, after, text.string(s, len)) + text.pos + wd <= ((margin - break_dist(ts, after)) max (before + breakgain))) + format(ts, before, after, text.blanks(wd)) + else format(ts, before, after, text.newline.blanks(before + ind)) + case Str(s, len) :: ts => format(ts, before, after, text.string(s, len)) } format(make_tree(input), 0, 0.0, Text()).result }