disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
authorwenzelm
Tue Aug 13 17:26:22 2013 +0200 (2013-08-13)
changeset 53016fa9c38891cf2
parent 53015 a1119cf551e8
child 53017 0f376701e83b
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
NEWS
src/Pure/General/symbol.ML
src/Pure/General/symbol_pos.ML
src/Pure/Syntax/lexicon.ML
src/Pure/term.ML
     1.1 --- a/NEWS	Tue Aug 13 16:25:47 2013 +0200
     1.2 +++ b/NEWS	Tue Aug 13 17:26:22 2013 +0200
     1.3 @@ -6,6 +6,17 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Simplified subscripts within identifiers, using plain \<^sub>
     1.8 +instead of the second copy \<^isub> and \<^isup>.  Superscripts are
     1.9 +only for literal tokens within notation; explicit mixfix annotations
    1.10 +for consts or fixed variables may be used as fall-back for unusual
    1.11 +names.  Obsolete \<twosuperior> has been expanded to \<^sup>2 in
    1.12 +Isabelle/HOL.  INCOMPATIBILITY, use "isabelle update_sub_sup" to
    1.13 +standardize symbols as a starting point for further manual cleanup.
    1.14 +The ML reference variable "legacy_isub_isup" may be set as temporary
    1.15 +workaround, to make the prover accept a subset of the old identifier
    1.16 +syntax.
    1.17 +
    1.18  * Uniform management of "quick_and_dirty" as system option (see also
    1.19  "isabelle options"), configuration option within the context (see also
    1.20  Config.get in Isabelle/ML), and attribute in Isabelle/Isar.  Minor
     2.1 --- a/src/Pure/General/symbol.ML	Tue Aug 13 16:25:47 2013 +0200
     2.2 +++ b/src/Pure/General/symbol.ML	Tue Aug 13 17:26:22 2013 +0200
     2.3 @@ -516,7 +516,8 @@
     2.4  (* bump string -- treat as base 26 or base 1 numbers *)
     2.5  
     2.6  fun symbolic_end (_ :: "\\<^sub>" :: _) = true
     2.7 -  | symbolic_end (_ :: "\\<^isub>" :: _) = true
     2.8 +  | symbolic_end (_ :: "\\<^isub>" :: _) = true  (*legacy*)
     2.9 +  | symbolic_end (_ :: "\\<^isup>" :: _) = true  (*legacy*)
    2.10    | symbolic_end (s :: _) = is_symbolic s
    2.11    | symbolic_end [] = false;
    2.12  
     3.1 --- a/src/Pure/General/symbol_pos.ML	Tue Aug 13 16:25:47 2013 +0200
     3.2 +++ b/src/Pure/General/symbol_pos.ML	Tue Aug 13 17:26:22 2013 +0200
     3.3 @@ -4,6 +4,8 @@
     3.4  Symbols with explicit position information.
     3.5  *)
     3.6  
     3.7 +val legacy_isub_isup = Unsynchronized.ref false;
     3.8 +
     3.9  signature SYMBOL_POS =
    3.10  sig
    3.11    type T = Symbol.symbol * Position.T
    3.12 @@ -217,7 +219,11 @@
    3.13  
    3.14  val letter = Scan.one (symbol #> Symbol.is_letter);
    3.15  val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig);
    3.16 -val sub = Scan.one (symbol #> (fn s => s = "\\<^sub>" orelse s = "\\<^isub>"));
    3.17 +
    3.18 +val sub =
    3.19 +  Scan.one (symbol #> (fn s =>
    3.20 +    if ! legacy_isub_isup then s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>"
    3.21 +    else s = "\\<^sub>"));
    3.22  
    3.23  in
    3.24  
     4.1 --- a/src/Pure/Syntax/lexicon.ML	Tue Aug 13 16:25:47 2013 +0200
     4.2 +++ b/src/Pure/Syntax/lexicon.ML	Tue Aug 13 17:26:22 2013 +0200
     4.3 @@ -295,7 +295,8 @@
     4.4      fun idxname cs ds = (implode (rev cs), nat 0 ds);
     4.5      fun chop_idx [] ds = idxname [] ds
     4.6        | chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds
     4.7 -      | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds
     4.8 +      | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds  (*legacy*)
     4.9 +      | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds  (*legacy*)
    4.10        | chop_idx (c :: cs) ds =
    4.11            if Symbol.is_digit c then chop_idx cs (c :: ds)
    4.12            else idxname (c :: cs) ds;
     5.1 --- a/src/Pure/term.ML	Tue Aug 13 16:25:47 2013 +0200
     5.2 +++ b/src/Pure/term.ML	Tue Aug 13 17:26:22 2013 +0200
     5.3 @@ -979,7 +979,8 @@
     5.4      val dot =
     5.5        (case rev (Symbol.explode x) of
     5.6          _ :: "\\<^sub>" :: _ => false
     5.7 -      | _ :: "\\<^isub>" :: _ => false
     5.8 +      | _ :: "\\<^isub>" :: _ => false  (*legacy*)
     5.9 +      | _ :: "\\<^isup>" :: _ => false  (*legacy*)
    5.10        | c :: _ => Symbol.is_digit c
    5.11        | _ => true);
    5.12    in