lsp: added conversion of symbols for dynamic output so that decoration ranges consider vscode_unicode_symbols setting;

--- 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)