# HG changeset patch
# User wenzelm
# Date 1086433639 -7200
# Node ID 7efc14398e82130f5eab6766205e59afb8a16e52
# Parent  3f2144aebd76d8dc0a670ae7b1b59e808239eca9
added datatype sym, val decode: symbol -> sym;

diff -r 3f2144aebd76 -r 7efc14398e82 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Sat Jun 05 13:07:04 2004 +0200
+++ b/src/Pure/General/symbol.ML	Sat Jun 05 13:07:19 2004 +0200
@@ -30,6 +30,9 @@
   val is_raw: symbol -> bool
   val decode_raw: symbol -> string
   val encode_raw: string -> symbol list
+  datatype sym = Char of string | Sym of string | Ctrl of string | Raw of string
+  exception DECODE of string
+  val decode: symbol -> sym
   datatype kind = Letter | Digit | Quasi | Blank | Other
   val kind: symbol -> kind
   val is_letter: symbol -> bool
@@ -166,6 +169,20 @@
 end;
 
 
+(* symbol variants *)
+
+datatype sym = Char of string | Sym of string | Ctrl of string | Raw of string;
+
+exception DECODE of string;
+
+fun decode s =
+  if is_char s then Char s
+  else if is_raw s then Raw (decode_raw s)
+  else if String.isPrefix "\\<^" s then Ctrl (String.substring (s, 3, size s - 4))
+  else if String.isPrefix "\\<" s then Sym (String.substring (s, 2, size s - 3))
+  else raise DECODE s;   (*NB: no error message in order to avoid looping in output!*)
+
+
 (* standard symbol kinds *)
 
 datatype kind = Letter | Digit | Quasi | Blank | Other;