--- a/src/Tools/VSCode/src/language_server.scala Sun Aug 10 23:35:19 2025 +0200
+++ b/src/Tools/VSCode/src/language_server.scala Mon Aug 11 12:13:48 2025 +0200
@@ -227,7 +227,7 @@
private val syslog_messages =
Session.Consumer[Prover.Output](getClass.getName) {
- case output => channel.log_writeln(resources.output_xml_text(output.message))
+ case output => channel.log_writeln(resources.output_text(XML.content(output.message)))
}
--- a/src/Tools/VSCode/src/vscode_resources.scala Sun Aug 10 23:35:19 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Mon Aug 11 12:13:48 2025 +0200
@@ -334,8 +334,6 @@
def output_text(content: String): String = Symbol.output(unicode_symbols_output, content)
def output_edit(content: String): String = Symbol.output(unicode_symbols_edits, content)
- def output_xml_text(body: XML.Tree): String = output_text(XML.content(body))
-
def output_text_xml(body: XML.Body): XML.Body =
body.map {
case XML.Elem(markup, body) => XML.Elem(markup, output_text_xml(body))