--- a/src/Pure/General/symbol_pos.ML Fri Jul 12 13:12:21 2013 +0200
+++ b/src/Pure/General/symbol_pos.ML Wed Jul 10 16:25:26 2013 +0200
@@ -215,51 +215,19 @@
local
-val latin = Symbol.is_ascii_letter;
-val digit = Symbol.is_ascii_digit;
-fun underscore s = s = "_";
-fun prime s = s = "'";
-fun subscript s = s = "\\<^sub>" orelse s = "\\<^isub>";
-fun script s = s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>";
-fun special_letter s = Symbol.is_letter_symbol s andalso not (script s);
-
-val scan_plain = Scan.one ((latin orf digit orf prime) o symbol) >> single;
-val scan_digit = Scan.one (digit o symbol) >> single;
-val scan_prime = Scan.one (prime o symbol) >> single;
-val scan_extended =
- Scan.one ((latin orf digit orf prime orf underscore orf special_letter) o symbol) >> single;
-
-val scan_subscript =
- Scan.one (subscript o symbol) --
- Scan.one ((latin orf digit orf prime orf special_letter) o symbol)
- >> (fn (x, y) => [x, y]);
-
-val scan_ident_part1 =
- Scan.one (latin o symbol) ::: (Scan.repeat (scan_plain || scan_subscript) >> flat) ||
- Scan.one (special_letter o symbol) :::
- (Scan.repeat (scan_digit || scan_prime || scan_subscript) >> flat);
-
-val scan_ident_part2 =
- Scan.repeat1 (scan_plain || scan_subscript) >> flat ||
- scan_ident_part1;
+val letter = Scan.one (symbol #> Symbol.is_letter);
+val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig);
+val sub_sup =
+ Scan.one (symbol #>
+ (fn s => s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^sup>" orelse s = "\\<^isup>"));
in
-val scan_ident0 =
- Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
-
-val scan_ident1 =
- Scan.one ((latin orf special_letter) o symbol) :::
- (Scan.repeat (scan_extended || Scan.one (subscript o symbol) ::: scan_extended) >> flat);
-
-val scan_ident2 =
- scan_ident_part1 @@@
- (Scan.repeat (Scan.many1 (underscore o symbol) @@@ scan_ident_part2) >> flat);
+val scan_ident =
+ letter ::: (Scan.repeat (letdigs1 || sub_sup ::: letdigs1) >> flat);
end;
-val scan_ident = scan_ident0;
-
fun is_identifier s =
Symbol.is_ascii_identifier s orelse
(case try (Scan.finite stopper scan_ident) (explode (s, Position.none)) of