# HG changeset patch
# User wenzelm
# Date 1727191872 -7200
# Node ID bdb63d71bf07df355466b834043a463a00edfcdb
# Parent  30c7922ec862aa1c126a43197624f804c297319f
tuned;

diff -r 30c7922ec862 -r bdb63d71bf07 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Tue Sep 24 17:27:56 2024 +0200
+++ b/src/Pure/General/pretty.ML	Tue Sep 24 17:31:12 2024 +0200
@@ -118,10 +118,8 @@
 type 'a block = {markup: 'a, consistent: bool, indent: int}
 
 fun make_block ({markup, consistent, indent}: Markup.output block) body =
-  let
-    val context = ML_Pretty.markup_context markup;
-    val ind = short_nat indent;
-  in from_ML (ML_Pretty.PrettyBlock (ind, consistent, context, map to_ML body)) end;
+  let val context = ML_Pretty.markup_context markup
+  in from_ML (ML_Pretty.PrettyBlock (short_nat indent, consistent, context, map to_ML body)) end;
 
 fun markup_block ({markup, consistent, indent}: Markup.T block) body =
   make_block {markup = YXML.output_markup markup, consistent = consistent, indent = indent} body;
@@ -130,6 +128,12 @@
 
 fun mark m prt = if m = Markup.empty then prt else markup m [prt];
 
+fun markup_blocks ({markup, consistent, indent}: Markup.T list block) body =
+  let
+    val markups = filter_out Markup.is_empty markup;
+    val (ms, m) = if null markups then ([], Markup.empty) else split_last markups;
+  in fold_rev mark ms (markup_block {markup = m, consistent = consistent, indent = indent} body) end;
+
 fun blk (indent, body) =
   markup_block {markup = Markup.empty, consistent = false, indent = indent} body;
 
@@ -161,12 +165,6 @@
 val mark_position = mark o Position.markup;
 fun mark_str_position (pos, s) = mark_str (Position.markup pos, s);
 
-fun markup_blocks ({markup, consistent, indent}: Markup.T list block) body =
-  let
-    val markups = filter_out Markup.is_empty markup;
-    val (ms, m) = if null markups then ([], Markup.empty) else split_last markups;
-  in fold_rev mark ms (markup_block {markup = m, consistent = consistent, indent = indent} body) end;
-
 val item = markup Markup.item;
 val text_fold = markup Markup.text_fold;