1.1 --- a/src/Pure/General/symbol.ML	Sat Jun 05 13:07:04 2004 +0200
     1.2 +++ b/src/Pure/General/symbol.ML	Sat Jun 05 13:07:19 2004 +0200
     1.3 @@ -30,6 +30,9 @@
     1.4    val is_raw: symbol -> bool
     1.5    val decode_raw: symbol -> string
     1.6    val encode_raw: string -> symbol list
     1.7 +  datatype sym = Char of string | Sym of string | Ctrl of string | Raw of string
     1.8 +  exception DECODE of string
     1.9 +  val decode: symbol -> sym
    1.10    datatype kind = Letter | Digit | Quasi | Blank | Other
    1.11    val kind: symbol -> kind
    1.12    val is_letter: symbol -> bool
    1.13 @@ -166,6 +169,20 @@
    1.14  end;
    1.15  
    1.16  
    1.17 +(* symbol variants *)
    1.18 +
    1.19 +datatype sym = Char of string | Sym of string | Ctrl of string | Raw of string;
    1.20 +
    1.21 +exception DECODE of string;
    1.22 +
    1.23 +fun decode s =
    1.24 +  if is_char s then Char s
    1.25 +  else if is_raw s then Raw (decode_raw s)
    1.26 +  else if String.isPrefix "\\<^" s then Ctrl (String.substring (s, 3, size s - 4))
    1.27 +  else if String.isPrefix "\\<" s then Sym (String.substring (s, 2, size s - 3))
    1.28 +  else raise DECODE s;   (*NB: no error message in order to avoid looping in output!*)
    1.29 +
    1.30 +
    1.31  (* standard symbol kinds *)
    1.32  
    1.33  datatype kind = Letter | Digit | Quasi | Blank | Other;