# HG changeset patch
# User wenzelm
# Date 1515418005 -3600
# Node ID 17f9fa98ababce4056b952a682b3f2d4f3fc34db
# Parent  820f3cbae27aceeebe714a8a49b322789ba487cc
more operations;

diff -r 820f3cbae27a -r 17f9fa98abab src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Mon Jan 08 11:41:16 2018 +0100
+++ b/src/Pure/General/symbol.ML	Mon Jan 08 14:26:45 2018 +0100
@@ -45,6 +45,7 @@
   datatype sym =
     Char of string | UTF8 of string | Sym of string | Control of string | Malformed of string | EOF
   val decode: symbol -> sym
+  val encode: sym -> symbol
   datatype kind = Letter | Digit | Quasi | Blank | Other
   val kind: symbol -> kind
   val is_letter: symbol -> bool
@@ -211,6 +212,13 @@
   else if is_control s then Control (String.substring (s, 3, size s - 4))
   else Sym (String.substring (s, 2, size s - 3));
 
+fun encode (Char s) = s
+  | encode (UTF8 s) = s
+  | encode (Sym s) = "\092<" ^ s ^ ">"
+  | encode (Control s) = "\092<^" ^ s ^ ">"
+  | encode (Malformed s) = s
+  | encode EOF = "";
+
 
 (* standard symbol kinds *)