# HG changeset patch
# User wenzelm
# Date 1762096541 -3600
# Node ID 6b99e12be6b5a4dcc6c5f9106328097cd2cb66a8
# Parent  8260cd98a7bc03055dc49be35b74ac382a15a435
clarified output: no pretty-printing here;

diff -r 8260cd98a7bc -r 6b99e12be6b5 src/Tools/VSCode/src/vscode_sledgehammer.scala
--- a/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sun Nov 02 16:07:47 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sun Nov 02 16:15:41 2025 +0100
@@ -26,7 +26,7 @@
   }
 
   private def consume_output(output: Editor.Output): Unit = {
-    val content = XML.string_of_body(output.messages)
+    val content = XML.string_of_body(Pretty.unbreakable(output.messages))
     server.channel.write(LSP.Sledgehammer_Output(content))
   }