clarified signature: fewer operations;
authorwenzelm
Mon, 11 Aug 2025 12:13:48 +0200
changeset 82987 1143c65b5829
parent 82986 951e009e20f4
child 82988 71ffc2c22348
clarified signature: fewer operations;
src/Tools/VSCode/src/language_server.scala
src/Tools/VSCode/src/vscode_resources.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)))
     }
 
 
--- 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))