--- a/src/Pure/General/pretty.ML Sat Oct 05 22:46:21 2024 +0200
+++ b/src/Pure/General/pretty.ML Sun Oct 06 13:02:33 2024 +0200
@@ -422,10 +422,10 @@
fun out (Block ((bg, en), _, _, [], _)) = Bytes.add bg #> Bytes.add en
| out (Block ((bg, en), consistent, indent, prts, _)) =
Bytes.add bg #>
- markup_bytes (Markup.block consistent indent) (fold out prts) #>
+ markup_bytes (Markup.block {consistent = consistent, indent = indent}) (fold out prts) #>
Bytes.add en
| out (Break (false, wd, ind)) =
- markup_bytes (Markup.break wd ind) (output_spaces_bytes ops wd)
+ markup_bytes (Markup.break {width = wd, indent = ind}) (output_spaces_bytes ops wd)
| out (Break (true, _, _)) = Bytes.add (output_newline ops)
| out (Str (s, _)) = Bytes.add s;
in Bytes.build o out o output_tree ops false end;
--- a/src/Pure/General/pretty.scala Sat Oct 05 22:46:21 2024 +0200
+++ b/src/Pure/General/pretty.scala Sun Oct 06 13:02:33 2024 +0200
@@ -21,10 +21,10 @@
val bullet: XML.Body = XML.elem(Markup.BULLET, space) :: space
def block(body: XML.Body, consistent: Boolean = false, indent: Int = 2): XML.Tree =
- XML.Elem(Markup.Block(consistent, indent), body)
+ XML.Elem(Markup.Block(consistent = consistent, indent = indent), body)
def brk(width: Int, indent: Int = 0): XML.Tree =
- XML.Elem(Markup.Break(width, indent), spaces(width))
+ XML.Elem(Markup.Break(width = width, indent = indent), spaces(width))
val fbrk: XML.Tree = XML.newline
def fbreaks(ts: List[XML.Tree]): XML.Body = Library.separate(fbrk, ts)
--- a/src/Pure/PIDE/markup.ML Sat Oct 05 22:46:21 2024 +0200
+++ b/src/Pure/PIDE/markup.ML Sun Oct 06 13:02:33 2024 +0200
@@ -84,8 +84,8 @@
val block_properties: string list
val indentN: string
val widthN: string
- val blockN: string val block: bool -> int -> T
- val breakN: string val break: int -> 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
val wordsN: string val words: T
@@ -481,16 +481,16 @@
val widthN = "width";
val blockN = "block";
-fun block c i =
+fun block {consistent, indent} =
(blockN,
- (if c then [(consistentN, Value.print_bool c)] else []) @
- (if i <> 0 then [(indentN, Value.print_int i)] else []));
+ (if consistent then [(consistentN, Value.print_bool consistent)] else []) @
+ (if indent <> 0 then [(indentN, Value.print_int indent)] else []));
val breakN = "break";
-fun break w i =
+fun break {width, indent} =
(breakN,
- (if w <> 0 then [(widthN, Value.print_int w)] else []) @
- (if i <> 0 then [(indentN, Value.print_int i)] else []));
+ (if width <> 0 then [(widthN, Value.print_int width)] else []) @
+ (if indent <> 0 then [(indentN, Value.print_int indent)] else []));
val (fbreakN, fbreak) = markup_elem "fbreak";
--- a/src/Pure/PIDE/markup.scala Sat Oct 05 22:46:21 2024 +0200
+++ b/src/Pure/PIDE/markup.scala Sun Oct 06 13:02:33 2024 +0200
@@ -265,30 +265,30 @@
object Block {
val name = "block"
- def apply(c: Boolean, i: Int): Markup =
+ def apply(consistent: Boolean = false, indent: Int = 0): Markup =
Markup(name,
- (if (c) Consistent(c) else Nil) :::
- (if (i != 0) Indent(i) else Nil))
+ (if (consistent) Consistent(consistent) else Nil) :::
+ (if (indent != 0) Indent(indent) else Nil))
def unapply(markup: Markup): Option[(Boolean, Int)] =
if (markup.name == name) {
- val c = Consistent.get(markup.properties)
- val i = Indent.get(markup.properties)
- Some((c, i))
+ val consistent = Consistent.get(markup.properties)
+ val indent = Indent.get(markup.properties)
+ Some((consistent, indent))
}
else None
}
object Break {
val name = "break"
- def apply(w: Int, i: Int): Markup =
+ def apply(width: Int = 0, indent: Int = 0): Markup =
Markup(name,
- (if (w != 0) Width(w) else Nil) :::
- (if (i != 0) Indent(i) else Nil))
+ (if (width != 0) Width(width) else Nil) :::
+ (if (indent != 0) Indent(indent) else Nil))
def unapply(markup: Markup): Option[(Int, Int)] =
if (markup.name == name) {
- val w = Width.get(markup.properties)
- val i = Indent.get(markup.properties)
- Some((w, i))
+ val width = Width.get(markup.properties)
+ val indent = Indent.get(markup.properties)
+ Some((width, indent))
}
else None
}