--- 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;
--- 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
}