diff -r 06461d0d46e1 -r c681b1a7b78e src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Sat Oct 12 21:21:50 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Sat Oct 12 22:05:37 2024 +0200
@@ -10,6 +10,7 @@
   type block =
     {markup: Markup.T list, open_block: bool, consistent: bool, unbreakable: bool, indent: int}
   val block_indent: int -> block
+  val pretty_block: block -> Pretty.T list -> Pretty.T
   datatype xsymb =
     Delim of string |
     Argument of string * int |
@@ -69,6 +70,11 @@
 fun block_indent indent : block =
   {markup = [], open_block = false, consistent = false, unbreakable = false, indent = indent};
 
+fun pretty_block {markup, open_block, consistent, indent, unbreakable} body =
+  Pretty.markup_blocks
+    {markup = markup, open_block = open_block, consistent = consistent, indent = indent} body
+  |> unbreakable ? Pretty.unbreakable;
+
 datatype xsymb =
   Delim of string |
   Argument of string * int |