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