src/Pure/General/symbol_pos.ML
changeset 50493 2bf3bfbb422d
parent 50295 3d6a4135a54f
child 52616 3ac2878764f9
     1.1 --- a/src/Pure/General/symbol_pos.ML	Wed Dec 12 16:28:18 2012 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Wed Dec 12 17:44:10 2012 +0100
     1.3 @@ -37,7 +37,6 @@
     1.4    val range: T list -> Position.range
     1.5    val implode_range: Position.T -> Position.T -> T list -> text * Position.range
     1.6    val explode: text * Position.T -> T list
     1.7 -  val scan_new_ident: T list -> T list * T list
     1.8    val scan_ident: T list -> T list * T list
     1.9    val is_identifier: string -> bool
    1.10  end;
    1.11 @@ -220,36 +219,46 @@
    1.12  val digit = Symbol.is_ascii_digit;
    1.13  fun underscore s = s = "_";
    1.14  fun prime s = s = "'";
    1.15 -fun script s = s = "\\<^sub>" orelse s = "\\<^isub>";
    1.16 +fun subscript s = s = "\\<^sub>" orelse s = "\\<^isub>";
    1.17 +fun script s = s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>";
    1.18  fun special_letter s = Symbol.is_letter_symbol s andalso not (script s);
    1.19  
    1.20  val scan_plain = Scan.one ((latin orf digit orf prime) o symbol) >> single;
    1.21  val scan_digit = Scan.one (digit o symbol) >> single;
    1.22  val scan_prime = Scan.one (prime o symbol) >> single;
    1.23 +val scan_extended =
    1.24 +  Scan.one ((latin orf digit orf prime orf underscore orf special_letter) o symbol) >> single;
    1.25  
    1.26 -val scan_script =
    1.27 -  Scan.one (script o symbol) -- Scan.one ((latin orf digit orf prime orf special_letter) o symbol)
    1.28 +val scan_subscript =
    1.29 +  Scan.one (subscript o symbol) --
    1.30 +  Scan.one ((latin orf digit orf prime orf special_letter) o symbol)
    1.31    >> (fn (x, y) => [x, y]);
    1.32  
    1.33  val scan_ident_part1 =
    1.34 -  Scan.one (latin o symbol) ::: (Scan.repeat (scan_plain || scan_script) >> flat) ||
    1.35 +  Scan.one (latin o symbol) ::: (Scan.repeat (scan_plain || scan_subscript) >> flat) ||
    1.36    Scan.one (special_letter o symbol) :::
    1.37 -    (Scan.repeat (scan_digit || scan_prime || scan_script) >> flat);
    1.38 +    (Scan.repeat (scan_digit || scan_prime || scan_subscript) >> flat);
    1.39  
    1.40  val scan_ident_part2 =
    1.41 -  Scan.repeat1 (scan_plain || scan_script) >> flat ||
    1.42 +  Scan.repeat1 (scan_plain || scan_subscript) >> flat ||
    1.43    scan_ident_part1;
    1.44  
    1.45  in
    1.46  
    1.47 -val scan_new_ident =
    1.48 +val scan_ident0 =
    1.49 +  Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
    1.50 +
    1.51 +val scan_ident1 =
    1.52 +  Scan.one ((latin orf special_letter) o symbol) :::
    1.53 +    (Scan.repeat (scan_extended || Scan.one (subscript o symbol) ::: scan_extended) >> flat);
    1.54 +
    1.55 +val scan_ident2 =
    1.56    scan_ident_part1 @@@
    1.57      (Scan.repeat (Scan.many1 (underscore o symbol) @@@ scan_ident_part2) >> flat);
    1.58  
    1.59  end;
    1.60  
    1.61 -val scan_ident =
    1.62 -  Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
    1.63 +val scan_ident = scan_ident0;
    1.64  
    1.65  fun is_identifier s =
    1.66    Symbol.is_ascii_identifier s orelse