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