src/Pure/PIDE/markup.ML
changeset 81267 d5ad89fda714
parent 81121 7cacedbddba7
child 81558 b57996a0688c
--- 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 []));