| changeset 72866 | 1d21b4c8023d |
| parent 72761 | 4519eeefe3b5 |
| child 73340 | 0ffcad1f6130 |
--- a/src/Tools/VSCode/src/vscode_resources.scala Thu Dec 10 14:51:56 2020 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Thu Dec 10 15:08:31 2020 +0100 @@ -337,8 +337,8 @@ /* output text */ - def output_text(s: String): String = - if (unicode_symbols) Symbol.decode(s) else Symbol.encode(s) + def output_text(text: String): String = + Symbol.output(unicode_symbols, text) def output_xml(xml: XML.Tree): String = output_text(XML.content(xml))