# HG changeset patch
# User wenzelm
# Date 1725450957 -7200
# Node ID b41c19523a2eeb9d615424e5c88e246052799201
# Parent  24339db7d22f829e276e8d8364e5824b7f734b87
tuned signature;

diff -r 24339db7d22f -r b41c19523a2e src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Wed Sep 04 12:50:52 2024 +0200
+++ b/src/Pure/Build/build.scala	Wed Sep 04 13:55:57 2024 +0200
@@ -837,7 +837,7 @@
                           margin = margin, breakgain = breakgain, metric = metric)
                       val ok =
                         check(message_head, Protocol.message_heading(elem, pos)) &&
-                        check(message_body, XML.content(Pretty.unformatted(List(elem))))
+                        check(message_body, Pretty.unformatted_string_of(List(elem)))
                       if (ok) buffer += message_text
                     }
                     if (buffer.nonEmpty) {
diff -r 24339db7d22f -r b41c19523a2e src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Wed Sep 04 12:50:52 2024 +0200
+++ b/src/Pure/General/pretty.scala	Wed Sep 04 13:55:57 2024 +0200
@@ -100,19 +100,17 @@
 
   /* unformatted output */
 
-  def unformatted(input: XML.Body): XML.Body = {
+  def unbreakable(input: XML.Body): XML.Body =
     input flatMap {
       case XML.Wrapped_Elem(markup, body1, body2) =>
-        List(XML.Wrapped_Elem(markup, body1, unformatted(body2)))
-      case XML.Elem(markup, body) =>
-        markup match {
-          case Markup.Block(_, _) => unformatted(body)
-          case Markup.Break(width, _) => XML.string(Symbol.spaces(width))
-          case _ => List(XML.Elem(markup, unformatted(body)))
-        }
+        List(XML.Wrapped_Elem(markup, body1, unbreakable(body2)))
+      case XML.Elem(Markup.Break(width, _), _) => spaces(width)
+      case XML.Elem(markup, body) => List(XML.Elem(markup, unbreakable(body)))
       case XML.Text(text) => XML.string(split_lines(text).mkString(Symbol.space))
     }
-  }
+
+  def unformatted_string_of(input: XML.Body): String =
+    XML.content(unbreakable(input))
 
 
   /* formatted output */