--- a/src/Pure/General/symbol.scala Thu Dec 10 14:51:56 2020 +0100
+++ b/src/Pure/General/symbol.scala Thu Dec 10 15:08:31 2020 +0100
@@ -537,6 +537,9 @@
}
}
+ def output(unicode_symbols: Boolean, text: String): String =
+ if (unicode_symbols) Symbol.decode(text) else Symbol.encode(text)
+
def fonts: Map[Symbol, String] = symbols.fonts
def font_names: List[String] = symbols.font_names
def font_index: Map[String, Int] = symbols.font_index
--- a/src/Pure/Tools/server_commands.scala Thu Dec 10 14:51:56 2020 +0100
+++ b/src/Pure/Tools/server_commands.scala Thu Dec 10 15:08:31 2020 +0100
@@ -237,8 +237,8 @@
args.commit_cleanup_delay.getOrElse(session.default_commit_cleanup_delay),
id = id, progress = progress)
- def output_text(s: String): String =
- if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s)
+ def output_text(text: String): String =
+ Symbol.output(args.unicode_symbols, text)
def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T =
{
--- 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))