# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1715785462 -7200
# Node ID d3e0d68c50d812bd286c4710f1280fa4f1d5c83f
# Parent  9c5a4ba4ced6c26fc99f58feee0642347eb6fb4d
lsp: added conversion of symbols for dynamic output so that decoration ranges consider vscode_unicode_symbols setting;

diff -r 9c5a4ba4ced6 -r d3e0d68c50d8 src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Wed May 15 16:54:39 2024 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Wed May 15 17:04:22 2024 +0200
@@ -58,8 +58,15 @@
         } else {
           val separate = Pretty.separate(st1.output)
           val formatted = Pretty.formatted(separate, margin = margin)
-          val tree = Markup_Tree.from_XML(formatted)
 
+          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(Symbol.output(resources.unicode_symbols, content))
+            }
+          }
+
+          val tree = Markup_Tree.from_XML(convert_symbols(formatted))
           val output = resources.output_pretty(separate, margin = margin)
 
           val document = Line.Document(output)