diff -r ac1e8686e523 -r 756fa442b7f3 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu Sep 19 20:38:19 2024 +0200
+++ b/src/Pure/General/pretty.ML	Thu Sep 19 20:38:34 2024 +0200
@@ -30,6 +30,7 @@
   type 'a block = {markup: 'a, consistent: bool, indent: int}
   val make_block: Markup.output block -> T list -> T
   val markup_block: Markup.T block -> T list -> T
+  val markup_blocks: Markup.T list block -> T list -> T
   val markup: Markup.T -> T list -> T
   val blk: int * T list -> T
   val block0: T list -> T
@@ -161,6 +162,12 @@
 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;