--- 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
}