--- a/src/Pure/PIDE/protocol.scala Thu Sep 12 14:38:19 2024 +0200
+++ b/src/Pure/PIDE/protocol.scala Thu Sep 12 14:42:04 2024 +0200
@@ -189,8 +189,8 @@
val text1 = if (heading) "\n" + message_heading(elem, pos) + ":\n" else ""
val body =
- Pretty.string_of(Protocol_Message.expose_no_reports(List(elem)),
- margin = margin, breakgain = breakgain, metric = metric)
+ Pretty.string_of(List(elem), margin = margin, breakgain = breakgain,
+ metric = metric, pure = true)
val text2 =
if (is_warning(elem) || is_legacy(elem)) Output.warning_prefix(body)