src/Pure/General/symbol_pos.ML
changeset 53016 fa9c38891cf2
parent 52920 4539e4a06339
child 54732 b01bb3d09928
     1.1 --- a/src/Pure/General/symbol_pos.ML	Tue Aug 13 16:25:47 2013 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Tue Aug 13 17:26:22 2013 +0200
     1.3 @@ -4,6 +4,8 @@
     1.4  Symbols with explicit position information.
     1.5  *)
     1.6  
     1.7 +val legacy_isub_isup = Unsynchronized.ref false;
     1.8 +
     1.9  signature SYMBOL_POS =
    1.10  sig
    1.11    type T = Symbol.symbol * Position.T
    1.12 @@ -217,7 +219,11 @@
    1.13  
    1.14  val letter = Scan.one (symbol #> Symbol.is_letter);
    1.15  val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig);
    1.16 -val sub = Scan.one (symbol #> (fn s => s = "\\<^sub>" orelse s = "\\<^isub>"));
    1.17 +
    1.18 +val sub =
    1.19 +  Scan.one (symbol #> (fn s =>
    1.20 +    if ! legacy_isub_isup then s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>"
    1.21 +    else s = "\\<^sub>"));
    1.22  
    1.23  in
    1.24