--- a/src/Pure/General/symbol.ML Tue Apr 28 13:34:48 2009 +0200
+++ b/src/Pure/General/symbol.ML Tue Apr 28 18:42:26 2009 +0200
@@ -18,6 +18,7 @@
val is_symbolic: symbol -> bool
val is_printable: symbol -> bool
val is_utf8_trailer: symbol -> bool
+ val name_of: symbol -> string
val eof: symbol
val is_eof: symbol -> bool
val not_eof: symbol -> bool
@@ -135,6 +136,10 @@
fun is_regular s =
not_eof s andalso s <> sync andalso s <> malformed andalso s <> end_malformed;
+fun name_of s = if is_symbolic s
+ then (unsuffix ">" o unprefix "\\<") s
+ else error (malformed_msg s);
+
(* ascii symbols *)