# HG changeset patch
# User wenzelm
# Date 1754907228 -7200
# Node ID 1143c65b58292825709408d347ecd23821250bfb
# Parent  951e009e20f4cba7c9f1685270f964af4ffd5359
clarified signature: fewer operations;

diff -r 951e009e20f4 -r 1143c65b5829 src/Tools/VSCode/src/language_server.scala
--- 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)))
     }
 
 
diff -r 951e009e20f4 -r 1143c65b5829 src/Tools/VSCode/src/vscode_resources.scala
--- 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))