--- a/src/Pure/Syntax/lexicon.ML Mon Apr 26 14:58:54 2004 +0200
+++ b/src/Pure/Syntax/lexicon.ML Mon Apr 26 15:00:20 2004 +0200
@@ -9,6 +9,7 @@
signature LEXICON0 =
sig
val is_identifier: string -> bool
+ val is_ascii_identifier: string -> bool
val implode_xstr: string list -> string
val explode_xstr: string -> string list
val scan_id: string list -> string * string list
@@ -66,7 +67,7 @@
val tokenize: Scan.lexicon -> bool -> string list -> token list
end;
-structure Lexicon : LEXICON =
+structure Lexicon: LEXICON =
struct
@@ -77,6 +78,10 @@
val is_identifier = is_ident o Symbol.explode;
+fun is_ascii_identifier s =
+ let val cs = Symbol.explode s
+ in forall Symbol.is_ascii cs andalso is_ident cs end;
+
fun is_xid s =
(case Symbol.explode s of
"_" :: cs => is_ident cs