# HG changeset patch
# User wenzelm
# Date 1754489832 -7200
# Node ID e879d01bcf451ed85a26e5dfcd995b5760810d53
# Parent  b66202c4e6d9ecb6ce95ae8bf5fad9445abc0351
clarified modules;

diff -r b66202c4e6d9 -r e879d01bcf45 src/Tools/VSCode/src/pretty_text_panel.scala
--- a/src/Tools/VSCode/src/pretty_text_panel.scala	Wed Aug 06 15:40:42 2025 +0200
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala	Wed Aug 06 16:17:12 2025 +0200
@@ -63,20 +63,13 @@
         channel.write(message)
       }
       else {
-        def convert_symbols(body: XML.Body): XML.Body =
-          body.map {
-            case XML.Elem(markup, body) => XML.Elem(markup, convert_symbols(body))
-            case XML.Text(content) => XML.Text(resources.output_text(content))
-          }
+        val converted = resources.output_text_xml(formatted)
+        val converted_tree = Markup_Tree.from_XML(converted)
+        val converted_text = XML.content(converted)
 
-        val converted = convert_symbols(formatted)
-
-        val tree = Markup_Tree.from_XML(converted)
-        val text = XML.content(converted)
-
-        val document = Line.Document(text)
+        val document = Line.Document(converted_text)
         val decorations =
-          tree.cumulate[Option[Markup]](Text.Range.full, None, Rendering.text_color_elements,
+          converted_tree.cumulate[Option[Markup]](Text.Range.full, None, Rendering.text_color_elements,
             { case (_, m) => Some(Some(m.info.markup)) }
           ).flatMap(info =>
               info.info match {
@@ -87,7 +80,7 @@
               }
           ).groupMap(_._2)(e => LSP.Decoration_Options(e._1, Nil)).toList
 
-        channel.write(output_json(text, Some(LSP.Decoration(decorations))))
+        channel.write(output_json(converted_text, Some(LSP.Decoration(decorations))))
       }
     }
   }
diff -r b66202c4e6d9 -r e879d01bcf45 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Aug 06 15:40:42 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Aug 06 16:17:12 2025 +0200
@@ -336,6 +336,12 @@
 
   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))
+      case XML.Text(content) => XML.Text(output_text(content))
+    }
+
   def output_pretty(body: XML.Body, margin: Double): String =
     output_text(Pretty.string_of(body, margin = margin, metric = Symbol.Metric))
   def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin)