# HG changeset patch
# User wenzelm
# Date 1725977198 -7200
# Node ID da20e00050abb9b18a45615cb8ece5533b0e7e09
# Parent  b569fbe1c262ef7ce1127e062ed51589f5c9780f
tuned comments, following Isabelle/ML;

diff -r b569fbe1c262 -r da20e00050ab src/Pure/General/pretty.scala
--- 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)