discontinued legacy_isub_isup;
authorwenzelm
Thu Dec 12 22:56:28 2013 +0100 (2013-12-12)
changeset 54732b01bb3d09928
parent 54731 384ac33802b0
child 54733 92fa590bdfe0
discontinued legacy_isub_isup;
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	Thu Dec 12 22:38:25 2013 +0100
     1.2 +++ b/NEWS	Thu Dec 12 22:56:28 2013 +0100
     1.3 @@ -12,6 +12,10 @@
     1.4  * Document antiquotation @{file_unchecked} is like @{file}, but does
     1.5  not check existence within the file-system.
     1.6  
     1.7 +* Discontinued legacy_isub_isup, which was a temporary Isabelle/ML
     1.8 +workaround in Isabelle2013-1.  The prover process no longer accepts
     1.9 +old identifier syntax with \<^isub> or \<^isup>.
    1.10 +
    1.11  
    1.12  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.13  
     2.1 --- a/src/Pure/General/symbol.ML	Thu Dec 12 22:38:25 2013 +0100
     2.2 +++ b/src/Pure/General/symbol.ML	Thu Dec 12 22:56:28 2013 +0100
     2.3 @@ -517,8 +517,6 @@
     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  (*legacy*)
     2.8 -  | symbolic_end (_ :: "\\<^isup>" :: _) = true  (*legacy*)
     2.9    | symbolic_end ("'" :: ss) = symbolic_end ss
    2.10    | symbolic_end (s :: _) = is_symbolic s
    2.11    | symbolic_end [] = false;
     3.1 --- a/src/Pure/General/symbol_pos.ML	Thu Dec 12 22:38:25 2013 +0100
     3.2 +++ b/src/Pure/General/symbol_pos.ML	Thu Dec 12 22:56:28 2013 +0100
     3.3 @@ -220,10 +220,7 @@
     3.4  val letter = Scan.one (symbol #> Symbol.is_letter);
     3.5  val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig);
     3.6  
     3.7 -val sub =
     3.8 -  Scan.one (symbol #> (fn s =>
     3.9 -    if ! legacy_isub_isup then s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>"
    3.10 -    else s = "\\<^sub>"));
    3.11 +val sub = Scan.one (symbol #> (fn s => s = "\\<^sub>"));
    3.12  
    3.13  in
    3.14  
     4.1 --- a/src/Pure/Syntax/lexicon.ML	Thu Dec 12 22:38:25 2013 +0100
     4.2 +++ b/src/Pure/Syntax/lexicon.ML	Thu Dec 12 22:56:28 2013 +0100
     4.3 @@ -295,8 +295,6 @@
     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  (*legacy*)
     4.8 -      | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds  (*legacy*)
     4.9        | chop_idx (c :: cs) ds =
    4.10            if Symbol.is_digit c then chop_idx cs (c :: ds)
    4.11            else idxname (c :: cs) ds;
     5.1 --- a/src/Pure/term.ML	Thu Dec 12 22:38:25 2013 +0100
     5.2 +++ b/src/Pure/term.ML	Thu Dec 12 22:56:28 2013 +0100
     5.3 @@ -979,8 +979,6 @@
     5.4      val dot =
     5.5        (case rev (Symbol.explode x) of
     5.6          _ :: "\\<^sub>" :: _ => false
     5.7 -      | _ :: "\\<^isub>" :: _ => false  (*legacy*)
     5.8 -      | _ :: "\\<^isup>" :: _ => false  (*legacy*)
     5.9        | c :: _ => Symbol.is_digit c
    5.10        | _ => true);
    5.11    in