more uniform Symbol.is_ascii_identifier in ML/Scala;

--- a/src/Pure/General/symbol.ML	Mon Nov 26 20:58:41 2012 +0100
+++ b/src/Pure/General/symbol.ML	Mon Nov 26 21:10:42 2012 +0100
@@ -35,6 +35,7 @@
   val is_ascii_upper: symbol -> bool
   val to_ascii_lower: symbol -> symbol
   val to_ascii_upper: symbol -> symbol
+  val is_ascii_identifier: string -> bool
   val scan_ascii_id: string list -> string * string list
   val is_raw: symbol -> bool
   val decode_raw: symbol -> string
@@ -161,6 +162,10 @@
 fun to_ascii_lower s = if is_ascii_upper s then chr (ord s + ord "a" - ord "A") else s;
 fun to_ascii_upper s = if is_ascii_lower s then chr (ord s + ord "A" - ord "a") else s;
 
+fun is_ascii_identifier s =
+  size s > 0 andalso is_ascii_letter (String.substring (s, 0, 1)) andalso
+  forall_string is_ascii_letdig s;
+
 val scan_ascii_id = Scan.one is_ascii_letter ^^ (Scan.many is_ascii_letdig >> implode);
 
 

--- a/src/Pure/General/symbol.scala	Mon Nov 26 20:58:41 2012 +0100
+++ b/src/Pure/General/symbol.scala	Mon Nov 26 21:10:42 2012 +0100
@@ -26,7 +26,7 @@
     is_ascii_letter(c) || is_ascii_digit(c) || is_ascii_quasi(c)
 
   def is_ascii_identifier(s: String): Boolean =
-    s.length > 0 && is_ascii_letter(s(0)) && s.substring(1).forall(is_ascii_letdig)
+    s.length > 0 && is_ascii_letter(s(0)) && s.forall(is_ascii_letdig)
 
 
   /* symbol matching */

--- a/src/Pure/ML/ml_syntax.ML	Mon Nov 26 20:58:41 2012 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Mon Nov 26 21:10:42 2012 +0100
@@ -34,7 +34,7 @@
 
 (* reserved words *)
 
-val reserved_names = filter Lexicon.is_ascii_identifier ML_Lex.keywords;
+val reserved_names = filter Symbol.is_ascii_identifier ML_Lex.keywords;
 val reserved = Name.make_context reserved_names;
 val is_reserved = Name.is_declared reserved;
 
@@ -42,7 +42,7 @@
 (* identifiers *)
 
 fun is_identifier name =
-  not (is_reserved name) andalso Lexicon.is_ascii_identifier name;
+  not (is_reserved name) andalso Symbol.is_ascii_identifier name;
 
 
 (* literal output -- unformatted *)

--- 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

--- a/src/Pure/Thy/latex.ML	Mon Nov 26 20:58:41 2012 +0100
+++ b/src/Pure/Thy/latex.ML	Mon Nov 26 21:10:42 2012 +0100
@@ -115,7 +115,7 @@
     if invisible_token tok then ""
     else if Token.is_command tok then
       "\\isacommand{" ^ output_syms s ^ "}"
-    else if Token.is_kind Token.Keyword tok andalso Lexicon.is_ascii_identifier s then
+    else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then
       "\\isakeyword{" ^ output_syms s ^ "}"
     else if Token.is_kind Token.String tok then
       enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)

--- a/src/Pure/Thy/thy_syntax.ML	Mon Nov 26 20:58:41 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Mon Nov 26 21:10:42 2012 +0100
@@ -59,7 +59,7 @@
   | Token.EOF           => (Markup.control, "");
 
 fun token_markup tok =
-  if Token.keyword_with (not o Lexicon.is_ascii_identifier) tok
+  if Token.keyword_with (not o Symbol.is_ascii_identifier) tok
   then (Markup.operator, "")
   else
     let