src/Pure/General/symbol.ML
changeset 31013 69a476d6fea6
parent 29606 fedb8be05f24
child 31425 e8d5417a1831
     1.1 --- a/src/Pure/General/symbol.ML	Tue Apr 28 13:34:48 2009 +0200
     1.2 +++ b/src/Pure/General/symbol.ML	Tue Apr 28 18:42:26 2009 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4    val is_symbolic: symbol -> bool
     1.5    val is_printable: symbol -> bool
     1.6    val is_utf8_trailer: symbol -> bool
     1.7 +  val name_of: symbol -> string
     1.8    val eof: symbol
     1.9    val is_eof: symbol -> bool
    1.10    val not_eof: symbol -> bool
    1.11 @@ -135,6 +136,10 @@
    1.12  fun is_regular s =
    1.13    not_eof s andalso s <> sync andalso s <> malformed andalso s <> end_malformed;
    1.14  
    1.15 +fun name_of s = if is_symbolic s
    1.16 +  then (unsuffix ">" o unprefix "\\<") s
    1.17 +  else error (malformed_msg s);
    1.18 +
    1.19  
    1.20  (* ascii symbols *)
    1.21