# HG changeset patch
# User wenzelm
# Date 1730024022 -3600
# Node ID d5ad89fda714cb6e2d65411c008d6126231f3850
# Parent  8300511f4c45cfbccd8eac84870906fcf4951b7b
clarified symbolic output: avoid redundant "block" element for open_block = true;

diff -r 8300511f4c45 -r d5ad89fda714 src/Pure/General/pretty.ML
--- 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)
diff -r 8300511f4c45 -r d5ad89fda714 src/Pure/PIDE/markup.ML
--- 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 []));