--- a/src/Pure/General/pretty.scala Tue Sep 10 16:03:42 2024 +0200
+++ b/src/Pure/General/pretty.scala Tue Sep 10 16:06:38 2024 +0200
@@ -98,7 +98,7 @@
}
- /* unformatted output */
+ /* no formatting */
def unbreakable(input: XML.Body): XML.Body =
input flatMap {
@@ -113,7 +113,7 @@
XML.content(unbreakable(input))
- /* formatted output */
+ /* formatting */
private sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0) {
def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1)