# HG changeset patch
# User wenzelm
# Date 1730101711 -3600
# Node ID 108284c8cbfded6f769326b230743997218b5f93
# Parent  c1e418161aceae593f7ae6fa4ded6cea8c3f1b76
removed obsolete markup for "open_block" (see also d5ad89fda714): Isabelle/Scala directly supports XML.Elem pretty-printing;

diff -r c1e418161ace -r 108284c8cbfd src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sun Oct 27 22:35:02 2024 +0100
+++ b/src/Pure/General/pretty.scala	Mon Oct 28 08:48:31 2024 +0100
@@ -21,13 +21,9 @@
   val bullet: XML.Body = XML.elem(Markup.BULLET, space) :: space
 
   def block(body: XML.Body,
-    open_block: Boolean = false,
     consistent: Boolean = false,
     indent: Int = 2
-  ): XML.Tree = {
-    val markup = Markup.Block(open_block = open_block, consistent = consistent, indent = indent)
-    XML.Elem(markup, body)
-  }
+  ): XML.Tree = XML.Elem(Markup.Block(consistent = consistent, indent = indent), body)
 
   def brk(width: Int, indent: Int = 0): XML.Tree =
     XML.Elem(Markup.Break(width = width, indent = indent), spaces(width))
@@ -169,10 +165,10 @@
           List(make_block(make_tree(body2), markup = markup, markup_body = Some(body1)))
         case XML.Elem(markup, body) =>
           markup match {
-            case Markup.Block(open_block, consistent, indent) =>
+            case Markup.Block(consistent, indent) =>
               List(
                 make_block(make_tree(body),
-                  open_block = open_block, consistent = consistent, indent = indent))
+                  consistent = consistent, indent = indent, open_block = false))
             case Markup.Break(width, indent) =>
               List(Break(false, force_nat(width), force_nat(indent)))
             case Markup(Markup.ITEM, _) =>
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
   }