--- a/src/Pure/Syntax/lexicon.ML Mon Nov 26 20:58:41 2012 +0100
+++ b/src/Pure/Syntax/lexicon.ML Mon Nov 26 21:10:42 2012 +0100
@@ -13,7 +13,6 @@
val var: indexname -> term
end
val is_identifier: string -> bool
- val is_ascii_identifier: string -> bool
val is_xid: string -> bool
val is_tid: string -> bool
val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
@@ -95,10 +94,6 @@
val is_identifier = Symbol.is_ident o Symbol.explode;
-fun is_ascii_identifier s =
- let val cs = Symbol.explode s
- in forall Symbol.is_ascii cs andalso Symbol.is_ident cs end;
-
fun is_xid s =
(case Symbol.explode s of
"_" :: cs => Symbol.is_ident cs
@@ -190,7 +185,7 @@
(* markup *)
fun literal_markup s =
- if is_ascii_identifier s then Markup.literal else Markup.delimiter;
+ if Symbol.is_ascii_identifier s then Markup.literal else Markup.delimiter;
val token_kind_markup =
fn VarSy => Markup.var