discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
authorwenzelm
Tue Aug 13 20:34:46 2013 +0200 (2013-08-13)
changeset 53021d0fa3f446b9d
parent 53020 afdabfeb5e94
child 53022 5f4703de4140
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
document antiquotations: renamed term style "isub" to "sub";
NEWS
etc/symbols
lib/texinputs/isabelle.sty
src/HOL/Tools/Nitpick/nitpick_util.ML
src/Pure/General/scan.scala
src/Pure/General/symbol.scala
src/Pure/Thy/html.ML
src/Pure/Thy/term_style.ML
src/Tools/WWW_Find/html_unicode.ML
src/Tools/jEdit/README.html
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/jEdit.props
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/NEWS	Tue Aug 13 19:52:12 2013 +0200
     1.2 +++ b/NEWS	Tue Aug 13 20:34:46 2013 +0200
     1.3 @@ -17,6 +17,9 @@
     1.4  workaround, to make the prover accept a subset of the old identifier
     1.5  syntax.
     1.6  
     1.7 +* Document antiquotations: term style "isub" has been renamed to
     1.8 +"sub".  Minor INCOMPATIBILITY.
     1.9 +
    1.10  * Uniform management of "quick_and_dirty" as system option (see also
    1.11  "isabelle options"), configuration option within the context (see also
    1.12  Config.get in Isabelle/ML), and attribute in Isabelle/Isar.  Minor
     2.1 --- a/etc/symbols	Tue Aug 13 19:52:12 2013 +0200
     2.2 +++ b/etc/symbols	Tue Aug 13 20:34:46 2013 +0200
     2.3 @@ -352,8 +352,6 @@
     2.4  \<some>                 code: 0x0003f5
     2.5  \<^sub>                 code: 0x0021e9  group: control  font: IsabelleText  abbrev: =_
     2.6  \<^sup>                 code: 0x0021e7  group: control  font: IsabelleText  abbrev: =^
     2.7 -\<^isub>                code: 0x0021e3  group: control  font: IsabelleText  abbrev: -_
     2.8 -\<^isup>                code: 0x0021e1  group: control  font: IsabelleText  abbrev: -^
     2.9  \<^bold>                code: 0x002759  group: control  font: IsabelleText  abbrev: -.
    2.10  \<^bsub>                code: 0x0021d8  group: control_block  font: IsabelleText  abbrev: =_(
    2.11  \<^esub>                code: 0x0021d9  group: control_block  font: IsabelleText  abbrev: =_)
     3.1 --- a/lib/texinputs/isabelle.sty	Tue Aug 13 19:52:12 2013 +0200
     3.2 +++ b/lib/texinputs/isabelle.sty	Tue Aug 13 20:34:46 2013 +0200
     3.3 @@ -30,8 +30,6 @@
     3.4  \DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}}
     3.5  \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
     3.6  \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
     3.7 -\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
     3.8 -\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
     3.9  \DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript}
    3.10  \DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
    3.11  \DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Aug 13 19:52:12 2013 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Aug 13 20:34:46 2013 +0200
     4.3 @@ -238,9 +238,9 @@
     4.4  val parse_time_option = Sledgehammer_Util.parse_time_option
     4.5  val string_of_time = ATP_Util.string_of_time
     4.6  
     4.7 -val i_subscript = implode o map (prefix "\<^sub>") o Symbol.explode
     4.8 +val subscript = implode o map (prefix "\<^sub>") o Symbol.explode
     4.9  fun nat_subscript n =
    4.10 -  n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? i_subscript
    4.11 +  n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
    4.12  
    4.13  fun flip_polarity Pos = Neg
    4.14    | flip_polarity Neg = Pos
     5.1 --- a/src/Pure/General/scan.scala	Tue Aug 13 19:52:12 2013 +0200
     5.2 +++ b/src/Pure/General/scan.scala	Tue Aug 13 20:34:46 2013 +0200
     5.3 @@ -349,10 +349,7 @@
     5.4        : Parser[Token] =
     5.5      {
     5.6        val letdigs1 = many1(Symbol.is_letdig)
     5.7 -      val sub =
     5.8 -        one(s =>
     5.9 -          s == Symbol.sub_decoded || s == "\\<^sub>" ||
    5.10 -          s == Symbol.isub_decoded || s == "\\<^isub>")
    5.11 +      val sub = one(s => s == Symbol.sub_decoded || s == "\\<^sub>")
    5.12        val id =
    5.13          one(Symbol.is_letter) ~
    5.14            (rep(letdigs1 | (sub ~ letdigs1 ^^ { case x ~ y => x + y })) ^^ (_.mkString)) ^^
     6.1 --- a/src/Pure/General/symbol.scala	Tue Aug 13 19:52:12 2013 +0200
     6.2 +++ b/src/Pure/General/symbol.scala	Tue Aug 13 20:34:46 2013 +0200
     6.3 @@ -364,8 +364,6 @@
     6.4  
     6.5      val sub_decoded = decode("\\<^sub>")
     6.6      val sup_decoded = decode("\\<^sup>")
     6.7 -    val isub_decoded = decode("\\<^isub>")
     6.8 -    val isup_decoded = decode("\\<^isup>")
     6.9      val bsub_decoded = decode("\\<^bsub>")
    6.10      val esub_decoded = decode("\\<^esub>")
    6.11      val bsup_decoded = decode("\\<^bsup>")
    6.12 @@ -426,8 +424,6 @@
    6.13  
    6.14    def sub_decoded: Symbol = symbols.sub_decoded
    6.15    def sup_decoded: Symbol = symbols.sup_decoded
    6.16 -  def isub_decoded: Symbol = symbols.isub_decoded
    6.17 -  def isup_decoded: Symbol = symbols.isup_decoded
    6.18    def bsub_decoded: Symbol = symbols.bsub_decoded
    6.19    def esub_decoded: Symbol = symbols.esub_decoded
    6.20    def bsup_decoded: Symbol = symbols.bsup_decoded
     7.1 --- a/src/Pure/Thy/html.ML	Tue Aug 13 19:52:12 2013 +0200
     7.2 +++ b/src/Pure/Thy/html.ML	Tue Aug 13 20:34:46 2013 +0200
     7.3 @@ -223,9 +223,7 @@
     7.4            val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
     7.5            val ((w, s), r) =
     7.6              if s1 = "\\<^sub>" then (output_sub "&#8681;" s2, ss)
     7.7 -            else if s1 = "\\<^isub>" then (output_sub "&#8675;" s2, ss)
     7.8              else if s1 = "\\<^sup>" then (output_sup "&#8679;" s2, ss)
     7.9 -            else if s1 = "\\<^isup>" then (output_sup "&#8673;" s2, ss)
    7.10              else if s1 = "\\<^bold>" then (output_bold "&#10073;" s2, ss)
    7.11              else (output_sym s1, rest);
    7.12          in output_syms r (s :: result, width + w) end;
     8.1 --- a/src/Pure/Thy/term_style.ML	Tue Aug 13 19:52:12 2013 +0200
     8.2 +++ b/src/Pure/Thy/term_style.ML	Tue Aug 13 20:34:46 2013 +0200
     8.3 @@ -75,27 +75,27 @@
     8.4          " in propositon: " ^ Syntax.string_of_term ctxt t)
     8.5    end);
     8.6  
     8.7 -fun isub_symbols (d :: s :: ss) =
     8.8 +fun sub_symbols (d :: s :: ss) =
     8.9        if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\\<^") s)
    8.10 -      then d :: "\\<^isub>" :: isub_symbols (s :: ss)
    8.11 +      then d :: "\\<^sub>" :: sub_symbols (s :: ss)
    8.12        else d :: s :: ss
    8.13 -  | isub_symbols cs = cs;
    8.14 +  | sub_symbols cs = cs;
    8.15  
    8.16 -val isub_name = implode o rev o isub_symbols o rev o Symbol.explode;
    8.17 +val sub_name = implode o rev o sub_symbols o rev o Symbol.explode;
    8.18  
    8.19 -fun isub_term (Free (n, T)) = Free (isub_name n, T)
    8.20 -  | isub_term (Var ((n, idx), T)) =
    8.21 -      if idx <> 0 then Var ((isub_name (n ^ string_of_int idx), 0), T)
    8.22 -      else Var ((isub_name n, 0), T)
    8.23 -  | isub_term (t $ u) = isub_term t $ isub_term u
    8.24 -  | isub_term (Abs (n, T, b)) = Abs (isub_name n, T, isub_term b)
    8.25 -  | isub_term t = t;
    8.26 +fun sub_term (Free (n, T)) = Free (sub_name n, T)
    8.27 +  | sub_term (Var ((n, idx), T)) =
    8.28 +      if idx <> 0 then Var ((sub_name (n ^ string_of_int idx), 0), T)
    8.29 +      else Var ((sub_name n, 0), T)
    8.30 +  | sub_term (t $ u) = sub_term t $ sub_term u
    8.31 +  | sub_term (Abs (n, T, b)) = Abs (sub_name n, T, sub_term b)
    8.32 +  | sub_term t = t;
    8.33  
    8.34  val _ = Context.>> (Context.map_theory
    8.35   (setup "lhs" (style_lhs_rhs fst) #>
    8.36    setup "rhs" (style_lhs_rhs snd) #>
    8.37    setup "prem" style_prem #>
    8.38    setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
    8.39 -  setup "isub" (Scan.succeed (K isub_term))));
    8.40 +  setup "sub" (Scan.succeed (K sub_term))));
    8.41  
    8.42  end;
     9.1 --- a/src/Tools/WWW_Find/html_unicode.ML	Tue Aug 13 19:52:12 2013 +0200
     9.2 +++ b/src/Tools/WWW_Find/html_unicode.ML	Tue Aug 13 20:34:46 2013 +0200
     9.3 @@ -52,9 +52,7 @@
     9.4    fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s);
     9.5  
     9.6    fun output_syms ("\<^sub>" :: s :: ss) = output_sub s :: output_syms ss
     9.7 -    | output_syms ("\<^isub>" :: s :: ss) = output_sub s :: output_syms ss
     9.8      | output_syms ("\<^sup>" :: s :: ss) = output_sup s :: output_syms ss
     9.9 -    | output_syms ("\<^isup>" :: s :: ss) = output_sup s :: output_syms ss
    9.10      | output_syms (s :: ss) = output_sym s :: output_syms ss
    9.11      | output_syms [] = [];
    9.12  
    10.1 --- a/src/Tools/jEdit/README.html	Tue Aug 13 19:52:12 2013 +0200
    10.2 +++ b/src/Tools/jEdit/README.html	Tue Aug 13 20:34:46 2013 +0200
    10.3 @@ -142,8 +142,6 @@
    10.4  
    10.5        <tr><td>sub</td>            <td><tt>=_</tt></td>          <td>⇩</td></tr>
    10.6        <tr><td>sup</td>            <td><tt>=^</tt></td>          <td>⇧</td></tr>
    10.7 -      <tr><td>isup</td>           <td><tt>-_</tt></td>          <td>⇣</td></tr>
    10.8 -      <tr><td>isub</td>           <td><tt>-^</tt></td>          <td>⇡</td></tr>
    10.9        <tr><td>bold</td>           <td><tt>-.</tt></td>          <td>❙</td></tr>
   10.10  
   10.11      </table>
    11.1 --- a/src/Tools/jEdit/src/actions.xml	Tue Aug 13 19:52:12 2013 +0200
    11.2 +++ b/src/Tools/jEdit/src/actions.xml	Tue Aug 13 20:34:46 2013 +0200
    11.3 @@ -122,16 +122,6 @@
    11.4  	    isabelle.jedit.Isabelle.control_sup(textArea);
    11.5  	  </CODE>
    11.6  	</ACTION>
    11.7 -	<ACTION NAME="isabelle.control-isub">
    11.8 -	  <CODE>
    11.9 -	    isabelle.jedit.Isabelle.control_isub(textArea);
   11.10 -	  </CODE>
   11.11 -	</ACTION>
   11.12 -	<ACTION NAME="isabelle.control-isup">
   11.13 -	  <CODE>
   11.14 -	    isabelle.jedit.Isabelle.control_isup(textArea);
   11.15 -	  </CODE>
   11.16 -	</ACTION>
   11.17  	<ACTION NAME="isabelle.control-bold">
   11.18  	  <CODE>
   11.19  	    isabelle.jedit.Isabelle.control_bold(textArea);
    12.1 --- a/src/Tools/jEdit/src/isabelle.scala	Tue Aug 13 19:52:12 2013 +0200
    12.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Tue Aug 13 20:34:46 2013 +0200
    12.3 @@ -140,12 +140,6 @@
    12.4    def control_sup(text_area: JEditTextArea)
    12.5    { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
    12.6  
    12.7 -  def control_isub(text_area: JEditTextArea)
    12.8 -  { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
    12.9 -
   12.10 -  def control_isup(text_area: JEditTextArea)
   12.11 -  { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
   12.12 -
   12.13    def control_bold(text_area: JEditTextArea)
   12.14    { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
   12.15  
    13.1 --- a/src/Tools/jEdit/src/jEdit.props	Tue Aug 13 19:52:12 2013 +0200
    13.2 +++ b/src/Tools/jEdit/src/jEdit.props	Tue Aug 13 20:34:46 2013 +0200
    13.3 @@ -188,8 +188,8 @@
    13.4  isabelle-theories.dock-position=right
    13.5  isabelle.control-bold.label=Control bold
    13.6  isabelle.control-bold.shortcut=C+e RIGHT
    13.7 -isabelle.control-isub.label=Control subscript
    13.8 -isabelle.control-isub.shortcut=C+e DOWN
    13.9 +isabelle.control-sub.label=Control subscript
   13.10 +isabelle.control-sub.shortcut=C+e DOWN
   13.11  isabelle.control-reset.label=Control reset
   13.12  isabelle.control-reset.shortcut=C+e LEFT
   13.13  isabelle.control-sup.label=Control superscript
    14.1 --- a/src/Tools/jEdit/src/token_markup.scala	Tue Aug 13 19:52:12 2013 +0200
    14.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Tue Aug 13 20:34:46 2013 +0200
    14.3 @@ -28,8 +28,7 @@
    14.4    /* editing support for control symbols */
    14.5  
    14.6    val is_control_style =
    14.7 -    Set(Symbol.sub_decoded, Symbol.sup_decoded,
    14.8 -      Symbol.isub_decoded, Symbol.isup_decoded, Symbol.bold_decoded)
    14.9 +    Set(Symbol.sub_decoded, Symbol.sup_decoded, Symbol.bold_decoded)
   14.10  
   14.11    def update_control_style(control: String, text: String): String =
   14.12    {
   14.13 @@ -161,8 +160,8 @@
   14.14    {
   14.15      // FIXME Symbol.bsub_decoded etc.
   14.16      def control_style(sym: String): Option[Byte => Byte] =
   14.17 -      if (sym == Symbol.sub_decoded || sym == Symbol.isub_decoded) Some(subscript(_))
   14.18 -      else if (sym == Symbol.sup_decoded || sym == Symbol.isup_decoded) Some(superscript(_))
   14.19 +      if (sym == Symbol.sub_decoded) Some(subscript(_))
   14.20 +      else if (sym == Symbol.sup_decoded) Some(superscript(_))
   14.21        else if (sym == Symbol.bold_decoded) Some(bold(_))
   14.22        else None
   14.23