disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
--- a/NEWS Tue Aug 13 16:25:47 2013 +0200
+++ b/NEWS Tue Aug 13 17:26:22 2013 +0200
@@ -6,6 +6,17 @@
*** General ***
+* Simplified subscripts within identifiers, using plain \<^sub>
+instead of the second copy \<^isub> and \<^isup>. Superscripts are
+only for literal tokens within notation; explicit mixfix annotations
+for consts or fixed variables may be used as fall-back for unusual
+names. Obsolete \<twosuperior> has been expanded to \<^sup>2 in
+Isabelle/HOL. INCOMPATIBILITY, use "isabelle update_sub_sup" to
+standardize symbols as a starting point for further manual cleanup.
+The ML reference variable "legacy_isub_isup" may be set as temporary
+workaround, to make the prover accept a subset of the old identifier
+syntax.
+
* Uniform management of "quick_and_dirty" as system option (see also
"isabelle options"), configuration option within the context (see also
Config.get in Isabelle/ML), and attribute in Isabelle/Isar. Minor
--- a/src/Pure/General/symbol.ML Tue Aug 13 16:25:47 2013 +0200
+++ b/src/Pure/General/symbol.ML Tue Aug 13 17:26:22 2013 +0200
@@ -516,7 +516,8 @@
(* bump string -- treat as base 26 or base 1 numbers *)
fun symbolic_end (_ :: "\\<^sub>" :: _) = true
- | symbolic_end (_ :: "\\<^isub>" :: _) = true
+ | symbolic_end (_ :: "\\<^isub>" :: _) = true (*legacy*)
+ | symbolic_end (_ :: "\\<^isup>" :: _) = true (*legacy*)
| symbolic_end (s :: _) = is_symbolic s
| symbolic_end [] = false;
--- 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
--- a/src/Pure/Syntax/lexicon.ML Tue Aug 13 16:25:47 2013 +0200
+++ b/src/Pure/Syntax/lexicon.ML Tue Aug 13 17:26:22 2013 +0200
@@ -295,7 +295,8 @@
fun idxname cs ds = (implode (rev cs), nat 0 ds);
fun chop_idx [] ds = idxname [] ds
| chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds
- | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds
+ | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds (*legacy*)
+ | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds (*legacy*)
| chop_idx (c :: cs) ds =
if Symbol.is_digit c then chop_idx cs (c :: ds)
else idxname (c :: cs) ds;
--- a/src/Pure/term.ML Tue Aug 13 16:25:47 2013 +0200
+++ b/src/Pure/term.ML Tue Aug 13 17:26:22 2013 +0200
@@ -979,7 +979,8 @@
val dot =
(case rev (Symbol.explode x) of
_ :: "\\<^sub>" :: _ => false
- | _ :: "\\<^isub>" :: _ => false
+ | _ :: "\\<^isub>" :: _ => false (*legacy*)
+ | _ :: "\\<^isup>" :: _ => false (*legacy*)
| c :: _ => Symbol.is_digit c
| _ => true);
in