src/Pure/General/symbol_pos.ML
changeset 53016 fa9c38891cf2
parent 52920 4539e4a06339
child 54732 b01bb3d09928
--- a/src/Pure/General/symbol_pos.ML	Tue Aug 13 16:25:47 2013 +0200
+++ b/src/Pure/General/symbol_pos.ML	Tue Aug 13 17:26:22 2013 +0200
@@ -4,6 +4,8 @@
 Symbols with explicit position information.
 *)
 
+val legacy_isub_isup = Unsynchronized.ref false;
+
 signature SYMBOL_POS =
 sig
   type T = Symbol.symbol * Position.T
@@ -217,7 +219,11 @@
 
 val letter = Scan.one (symbol #> Symbol.is_letter);
 val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig);
-val sub = Scan.one (symbol #> (fn s => s = "\\<^sub>" orelse s = "\\<^isub>"));
+
+val sub =
+  Scan.one (symbol #> (fn s =>
+    if ! legacy_isub_isup then s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>"
+    else s = "\\<^sub>"));
 
 in