tuned signature;
authorwenzelm
Thu, 10 Dec 2020 15:08:31 +0100
changeset 72866 1d21b4c8023d
parent 72865 ebf72a3b8daa
child 72867 7b10b40b1273
tuned signature;
src/Pure/General/symbol.scala
src/Pure/Tools/server_commands.scala
src/Tools/VSCode/src/vscode_resources.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
--- 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))