more systematic identifier variants to facilitate experimentation;

--- a/src/Pure/General/symbol_pos.ML	Wed Dec 12 16:28:18 2012 +0100
+++ b/src/Pure/General/symbol_pos.ML	Wed Dec 12 17:44:10 2012 +0100
@@ -37,7 +37,6 @@
   val range: T list -> Position.range
   val implode_range: Position.T -> Position.T -> T list -> text * Position.range
   val explode: text * Position.T -> T list
-  val scan_new_ident: T list -> T list * T list
   val scan_ident: T list -> T list * T list
   val is_identifier: string -> bool
 end;
@@ -220,36 +219,46 @@
 val digit = Symbol.is_ascii_digit;
 fun underscore s = s = "_";
 fun prime s = s = "'";
-fun script s = s = "\\<^sub>" orelse s = "\\<^isub>";
+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_script =
-  Scan.one (script o symbol) -- Scan.one ((latin orf digit orf prime orf special_letter) o symbol)
+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_script) >> flat) ||
+  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_script) >> flat);
+    (Scan.repeat (scan_digit || scan_prime || scan_subscript) >> flat);
 
 val scan_ident_part2 =
-  Scan.repeat1 (scan_plain || scan_script) >> flat ||
+  Scan.repeat1 (scan_plain || scan_subscript) >> flat ||
   scan_ident_part1;
 
 in
 
-val scan_new_ident =
+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);
 
 end;
 
-val scan_ident =
-  Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
+val scan_ident = scan_ident0;
 
 fun is_identifier s =
   Symbol.is_ascii_identifier s orelse