# HG changeset patch
# User wenzelm
# Date 1728212553 -7200
# Node ID 080beab272645363c446a408c8c7d7e069aad9ec
# Parent  faccef6c0806b2ff339591a7b6fac8ccce28d5f8
clarified signature;

diff -r faccef6c0806 -r 080beab27264 src/Pure/General/pretty.ML
--- 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;
diff -r faccef6c0806 -r 080beab27264 src/Pure/General/pretty.scala
--- 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)
diff -r faccef6c0806 -r 080beab27264 src/Pure/PIDE/markup.ML
--- 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";
 
diff -r faccef6c0806 -r 080beab27264 src/Pure/PIDE/markup.scala
--- 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
   }