--- a/NEWS Wed Aug 20 14:09:06 2025 +0200
+++ b/NEWS Thu Aug 21 12:11:38 2025 +0200
@@ -35,6 +35,9 @@
"show_results" (default true) and "show_states" (default false),
provided at build-time for the underlying session database.
+* For pretty-printed output a margin <= 0 means there is no margin to be
+observed: only forced breaks are taken.
+
*** Isabelle/jEdit Prover IDE ***
--- a/src/Pure/General/pretty.ML Wed Aug 20 14:09:06 2025 +0200
+++ b/src/Pure/General/pretty.ML Thu Aug 21 12:11:38 2025 +0200
@@ -416,8 +416,11 @@
fun format_tree (ops: output_ops) input =
let
val margin = #margin ops;
- val breakgain = margin div 20; (*minimum added space required of a break*)
- val emergencypos = margin div 2; (*position too far to right*)
+ val margin_defined = margin > 0;
+ val margin1 = if margin_defined then margin else ML_Pretty.default_margin;
+
+ val breakgain = margin1 div 20; (*minimum added space required of a break*)
+ val emergencypos = margin1 div 2; (*position too far to right*)
fun blanks_state n state = add_state (#1 (output_spaces ops n)) state;
val blanks = string o output_spaces ops;
@@ -457,12 +460,13 @@
val pos' = pos + indent;
val pos'' = pos' mod emergencypos;
val before' =
- if pos' < emergencypos
+ if not margin_defined orelse pos' < emergencypos
then (Option.map (close_state o blanks_state indent) (#line text), pos')
else (Option.map (fn _ => blanks_state pos'' init_state) (#line text), pos'');
val after' = break_dist (ts, after)
val body' = body
- |> (consistent andalso pos + blen > margin - after') ? map force_break;
+ |> (margin_defined andalso 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*)
@@ -473,7 +477,8 @@
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)
+ (not margin_defined orelse
+ pos + wd <= Int.max (margin - break_dist (ts, after), #2 before + breakgain))
then text |> blanks wd (*just insert wd blanks*)
else text |> break before |> blanks ind)
| Str str :: ts => format (ts, before, after) (string str text));
--- a/src/Pure/General/pretty.scala Wed Aug 20 14:09:06 2025 +0200
+++ b/src/Pure/General/pretty.scala Thu Aug 21 12:11:38 2025 +0200
@@ -223,7 +223,9 @@
breakgain: Double = default_breakgain,
metric: Metric = Codepoint.Metric
): XML.Body = {
- val emergencypos = (margin / 2).round.toInt
+ val margin_defined = margin > 0
+ val margin1 = if (margin_defined) margin else default_margin
+ val emergencypos = (margin1 / 2).round.toInt
def make_tree(inp: XML.Body): List[Tree] =
inp flatMap {
@@ -254,10 +256,12 @@
case (block: Block) :: ts =>
val pos1 = text.pos + block.indent
val pos2 = (pos1.round.toInt % emergencypos).toDouble
- val before1 = if (pos1 < emergencypos) pos1 else pos2
+ val before1 = if (!margin_defined || 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)
+ if (margin_defined && block.consistent && text.pos + block.length > margin - after1) {
+ force_all(block.body)
+ }
else block.body
val btext1 =
if (block.markup == no_markup) format(body1, before1, after1, text)
@@ -270,8 +274,10 @@
format(ts1, before, after, btext1)
case Break(force, wd, ind) :: ts =>
if (!force &&
- text.pos + wd <= ((margin - break_dist(ts, after)) max (before + breakgain)))
+ (!margin_defined ||
+ 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).ceil.toInt))
case Str(s, len) :: ts => format(ts, before, after, text.string(s, len))
}