# HG changeset patch
# User wenzelm
# Date 1082984420 -7200
# Node ID 6ed90bd68eda2b24581925b9036bd97c1d2ac077
# Parent  662b181cae059cee04594c167fe0fe6f613813db
added is_ascii_identifier;

diff -r 662b181cae05 -r 6ed90bd68eda src/Pure/Syntax/lexicon.ML
--- 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