# HG changeset patch
# User wenzelm
# Date 1607609311 -3600
# Node ID 1d21b4c8023da57c62ba07acaf09518babd167e0
# Parent  ebf72a3b8daae812897ebc5d359c6436f875e36a
tuned signature;

diff -r ebf72a3b8daa -r 1d21b4c8023d src/Pure/General/symbol.scala
--- 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
diff -r ebf72a3b8daa -r 1d21b4c8023d src/Pure/Tools/server_commands.scala
--- 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 =
       {
diff -r ebf72a3b8daa -r 1d21b4c8023d src/Tools/VSCode/src/vscode_resources.scala
--- 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))