clarified new identifier syntax: exclude \<^isup>, include subscripted prime (to allow imitating full identifier here);
authorwenzelm
Wed Nov 28 16:07:17 2012 +0100 (2012-11-28 ago)
changeset 5025341fd9f68614b
parent 50252 4aa34bd43228
child 50254 935ac0ad7e83
clarified new identifier syntax: exclude \<^isup>, include subscripted prime (to allow imitating full identifier here);
src/Pure/General/symbol_pos.ML
     1.1 --- a/src/Pure/General/symbol_pos.ML	Wed Nov 28 15:59:18 2012 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Wed Nov 28 16:07:17 2012 +0100
     1.3 @@ -220,7 +220,7 @@
     1.4  val digit = Symbol.is_ascii_digit;
     1.5  fun underscore s = s = "_";
     1.6  fun prime s = s = "'";
     1.7 -fun script s = s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>";
     1.8 +fun script s = s = "\\<^sub>" orelse s = "\\<^isub>";
     1.9  fun special_letter s = Symbol.is_letter_symbol s andalso not (script s);
    1.10  
    1.11  val scan_plain = Scan.one ((latin orf digit orf prime) o symbol) >> single;
    1.12 @@ -228,7 +228,7 @@
    1.13  val scan_prime = Scan.one (prime o symbol) >> single;
    1.14  
    1.15  val scan_script =
    1.16 -  Scan.one (script o symbol) -- Scan.one ((latin orf digit orf special_letter) o symbol)
    1.17 +  Scan.one (script o symbol) -- Scan.one ((latin orf digit orf prime orf special_letter) o symbol)
    1.18    >> (fn (x, y) => [x, y]);
    1.19  
    1.20  val scan_ident_part1 =