diff -r c1e418161ace -r 108284c8cbfd src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sun Oct 27 22:35:02 2024 +0100
+++ b/src/Pure/PIDE/markup.scala	Mon Oct 28 08:48:31 2024 +0100
@@ -259,24 +259,21 @@
 
   /* pretty printing */
 
-  val Open_Block = new Properties.Boolean("open_block")
   val Consistent = new Properties.Boolean("consistent")
   val Indent = new Properties.Int("indent")
   val Width = new Properties.Int("width")
 
   object Block {
     val name = "block"
-    def apply(open_block: Boolean = false, consistent: Boolean = false, indent: Int = 0): Markup =
+    def apply(consistent: Boolean = false, indent: Int = 0): Markup =
       Markup(name,
-        (if (open_block) Open_Block(open_block) else Nil) :::
         (if (consistent) Consistent(consistent) else Nil) :::
         (if (indent != 0) Indent(indent) else Nil))
-    def unapply(markup: Markup): Option[(Boolean, Boolean, Int)] =
+    def unapply(markup: Markup): Option[(Boolean, Int)] =
       if (markup.name == name) {
-        val open_block = Open_Block.get(markup.properties)
         val consistent = Consistent.get(markup.properties)
         val indent = Indent.get(markup.properties)
-        Some((open_block, consistent, indent))
+        Some((consistent, indent))
       }
       else None
   }