clarified symbolic output: avoid redundant "block" element for open_block = true;
--- a/src/Pure/General/pretty.ML Sun Oct 27 11:02:21 2024 +0100
+++ b/src/Pure/General/pretty.ML Sun Oct 27 11:13:42 2024 +0100
@@ -449,10 +449,10 @@
in Bytes.add bg #> body #> Bytes.add en end;
fun out (Block {markup = (bg, en), body = [], ...}) = Bytes.add bg #> Bytes.add en
- | out (Block {markup = (bg, en), open_block, consistent, indent, body = prts, ...}) =
- let
- val block_markup =
- Markup.block {open_block = open_block, consistent = consistent, indent = indent};
+ | out (Block {markup = (bg, en), open_block = true, body = prts, ...}) =
+ Bytes.add bg #> fold out prts #> Bytes.add en
+ | out (Block {markup = (bg, en), consistent, indent, body = prts, ...}) =
+ let val block_markup = Markup.block {consistent = consistent, indent = indent}
in Bytes.add bg #> markup_bytes block_markup (fold out prts) #> Bytes.add en end
| out (Break (false, wd, ind)) =
markup_bytes (Markup.break {width = wd, indent = ind}) (output_spaces_bytes ops wd)
--- a/src/Pure/PIDE/markup.ML Sun Oct 27 11:02:21 2024 +0100
+++ b/src/Pure/PIDE/markup.ML Sun Oct 27 11:13:42 2024 +0100
@@ -85,7 +85,7 @@
val block_properties: string list
val indentN: string
val widthN: string
- val blockN: string val block: {open_block: bool, consistent: bool, indent: int} -> T
+ val blockN: string val block: {consistent: bool, indent: int} -> T
val breakN: string val break: {width: int, indent: int} -> T
val fbreakN: string val fbreak: T
val itemN: string val item: T
@@ -483,9 +483,8 @@
val widthN = "width";
val blockN = "block";
-fun block {open_block, consistent, indent} =
+fun block {consistent, indent} =
(blockN,
- (if open_block then [(open_blockN, Value.print_bool open_block)] else []) @
(if consistent then [(consistentN, Value.print_bool consistent)] else []) @
(if indent <> 0 then [(indentN, Value.print_int indent)] else []));