discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
document antiquotations: renamed term style "isub" to "sub";
--- a/NEWS Tue Aug 13 19:52:12 2013 +0200
+++ b/NEWS Tue Aug 13 20:34:46 2013 +0200
@@ -17,6 +17,9 @@
workaround, to make the prover accept a subset of the old identifier
syntax.
+* Document antiquotations: term style "isub" has been renamed to
+"sub". Minor INCOMPATIBILITY.
+
* 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/etc/symbols Tue Aug 13 19:52:12 2013 +0200
+++ b/etc/symbols Tue Aug 13 20:34:46 2013 +0200
@@ -352,8 +352,6 @@
\<some> code: 0x0003f5
\<^sub> code: 0x0021e9 group: control font: IsabelleText abbrev: =_
\<^sup> code: 0x0021e7 group: control font: IsabelleText abbrev: =^
-\<^isub> code: 0x0021e3 group: control font: IsabelleText abbrev: -_
-\<^isup> code: 0x0021e1 group: control font: IsabelleText abbrev: -^
\<^bold> code: 0x002759 group: control font: IsabelleText abbrev: -.
\<^bsub> code: 0x0021d8 group: control_block font: IsabelleText abbrev: =_(
\<^esub> code: 0x0021d9 group: control_block font: IsabelleText abbrev: =_)
--- a/lib/texinputs/isabelle.sty Tue Aug 13 19:52:12 2013 +0200
+++ b/lib/texinputs/isabelle.sty Tue Aug 13 20:34:46 2013 +0200
@@ -30,8 +30,6 @@
\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}}
\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
-\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
-\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript}
\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Aug 13 19:52:12 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Aug 13 20:34:46 2013 +0200
@@ -238,9 +238,9 @@
val parse_time_option = Sledgehammer_Util.parse_time_option
val string_of_time = ATP_Util.string_of_time
-val i_subscript = implode o map (prefix "\<^sub>") o Symbol.explode
+val subscript = implode o map (prefix "\<^sub>") o Symbol.explode
fun nat_subscript n =
- n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? i_subscript
+ n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
fun flip_polarity Pos = Neg
| flip_polarity Neg = Pos
--- a/src/Pure/General/scan.scala Tue Aug 13 19:52:12 2013 +0200
+++ b/src/Pure/General/scan.scala Tue Aug 13 20:34:46 2013 +0200
@@ -349,10 +349,7 @@
: Parser[Token] =
{
val letdigs1 = many1(Symbol.is_letdig)
- val sub =
- one(s =>
- s == Symbol.sub_decoded || s == "\\<^sub>" ||
- s == Symbol.isub_decoded || s == "\\<^isub>")
+ val sub = one(s => s == Symbol.sub_decoded || s == "\\<^sub>")
val id =
one(Symbol.is_letter) ~
(rep(letdigs1 | (sub ~ letdigs1 ^^ { case x ~ y => x + y })) ^^ (_.mkString)) ^^
--- a/src/Pure/General/symbol.scala Tue Aug 13 19:52:12 2013 +0200
+++ b/src/Pure/General/symbol.scala Tue Aug 13 20:34:46 2013 +0200
@@ -364,8 +364,6 @@
val sub_decoded = decode("\\<^sub>")
val sup_decoded = decode("\\<^sup>")
- val isub_decoded = decode("\\<^isub>")
- val isup_decoded = decode("\\<^isup>")
val bsub_decoded = decode("\\<^bsub>")
val esub_decoded = decode("\\<^esub>")
val bsup_decoded = decode("\\<^bsup>")
@@ -426,8 +424,6 @@
def sub_decoded: Symbol = symbols.sub_decoded
def sup_decoded: Symbol = symbols.sup_decoded
- def isub_decoded: Symbol = symbols.isub_decoded
- def isup_decoded: Symbol = symbols.isup_decoded
def bsub_decoded: Symbol = symbols.bsub_decoded
def esub_decoded: Symbol = symbols.esub_decoded
def bsup_decoded: Symbol = symbols.bsup_decoded
--- a/src/Pure/Thy/html.ML Tue Aug 13 19:52:12 2013 +0200
+++ b/src/Pure/Thy/html.ML Tue Aug 13 20:34:46 2013 +0200
@@ -223,9 +223,7 @@
val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
val ((w, s), r) =
if s1 = "\\<^sub>" then (output_sub "⇩" s2, ss)
- else if s1 = "\\<^isub>" then (output_sub "⇣" s2, ss)
else if s1 = "\\<^sup>" then (output_sup "⇧" s2, ss)
- else if s1 = "\\<^isup>" then (output_sup "⇡" s2, ss)
else if s1 = "\\<^bold>" then (output_bold "❙" s2, ss)
else (output_sym s1, rest);
in output_syms r (s :: result, width + w) end;
--- a/src/Pure/Thy/term_style.ML Tue Aug 13 19:52:12 2013 +0200
+++ b/src/Pure/Thy/term_style.ML Tue Aug 13 20:34:46 2013 +0200
@@ -75,27 +75,27 @@
" in propositon: " ^ Syntax.string_of_term ctxt t)
end);
-fun isub_symbols (d :: s :: ss) =
+fun sub_symbols (d :: s :: ss) =
if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\\<^") s)
- then d :: "\\<^isub>" :: isub_symbols (s :: ss)
+ then d :: "\\<^sub>" :: sub_symbols (s :: ss)
else d :: s :: ss
- | isub_symbols cs = cs;
+ | sub_symbols cs = cs;
-val isub_name = implode o rev o isub_symbols o rev o Symbol.explode;
+val sub_name = implode o rev o sub_symbols o rev o Symbol.explode;
-fun isub_term (Free (n, T)) = Free (isub_name n, T)
- | isub_term (Var ((n, idx), T)) =
- if idx <> 0 then Var ((isub_name (n ^ string_of_int idx), 0), T)
- else Var ((isub_name n, 0), T)
- | isub_term (t $ u) = isub_term t $ isub_term u
- | isub_term (Abs (n, T, b)) = Abs (isub_name n, T, isub_term b)
- | isub_term t = t;
+fun sub_term (Free (n, T)) = Free (sub_name n, T)
+ | sub_term (Var ((n, idx), T)) =
+ if idx <> 0 then Var ((sub_name (n ^ string_of_int idx), 0), T)
+ else Var ((sub_name n, 0), T)
+ | sub_term (t $ u) = sub_term t $ sub_term u
+ | sub_term (Abs (n, T, b)) = Abs (sub_name n, T, sub_term b)
+ | sub_term t = t;
val _ = Context.>> (Context.map_theory
(setup "lhs" (style_lhs_rhs fst) #>
setup "rhs" (style_lhs_rhs snd) #>
setup "prem" style_prem #>
setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
- setup "isub" (Scan.succeed (K isub_term))));
+ setup "sub" (Scan.succeed (K sub_term))));
end;
--- a/src/Tools/WWW_Find/html_unicode.ML Tue Aug 13 19:52:12 2013 +0200
+++ b/src/Tools/WWW_Find/html_unicode.ML Tue Aug 13 20:34:46 2013 +0200
@@ -52,9 +52,7 @@
fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s);
fun output_syms ("\<^sub>" :: s :: ss) = output_sub s :: output_syms ss
- | output_syms ("\<^isub>" :: s :: ss) = output_sub s :: output_syms ss
| output_syms ("\<^sup>" :: s :: ss) = output_sup s :: output_syms ss
- | output_syms ("\<^isup>" :: s :: ss) = output_sup s :: output_syms ss
| output_syms (s :: ss) = output_sym s :: output_syms ss
| output_syms [] = [];
--- a/src/Tools/jEdit/README.html Tue Aug 13 19:52:12 2013 +0200
+++ b/src/Tools/jEdit/README.html Tue Aug 13 20:34:46 2013 +0200
@@ -142,8 +142,6 @@
<tr><td>sub</td> <td><tt>=_</tt></td> <td>⇩</td></tr>
<tr><td>sup</td> <td><tt>=^</tt></td> <td>⇧</td></tr>
- <tr><td>isup</td> <td><tt>-_</tt></td> <td>⇣</td></tr>
- <tr><td>isub</td> <td><tt>-^</tt></td> <td>⇡</td></tr>
<tr><td>bold</td> <td><tt>-.</tt></td> <td>❙</td></tr>
</table>
--- a/src/Tools/jEdit/src/actions.xml Tue Aug 13 19:52:12 2013 +0200
+++ b/src/Tools/jEdit/src/actions.xml Tue Aug 13 20:34:46 2013 +0200
@@ -122,16 +122,6 @@
isabelle.jedit.Isabelle.control_sup(textArea);
</CODE>
</ACTION>
- <ACTION NAME="isabelle.control-isub">
- <CODE>
- isabelle.jedit.Isabelle.control_isub(textArea);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.control-isup">
- <CODE>
- isabelle.jedit.Isabelle.control_isup(textArea);
- </CODE>
- </ACTION>
<ACTION NAME="isabelle.control-bold">
<CODE>
isabelle.jedit.Isabelle.control_bold(textArea);
--- a/src/Tools/jEdit/src/isabelle.scala Tue Aug 13 19:52:12 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Tue Aug 13 20:34:46 2013 +0200
@@ -140,12 +140,6 @@
def control_sup(text_area: JEditTextArea)
{ Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
- def control_isub(text_area: JEditTextArea)
- { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
-
- def control_isup(text_area: JEditTextArea)
- { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
-
def control_bold(text_area: JEditTextArea)
{ Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
--- a/src/Tools/jEdit/src/jEdit.props Tue Aug 13 19:52:12 2013 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Tue Aug 13 20:34:46 2013 +0200
@@ -188,8 +188,8 @@
isabelle-theories.dock-position=right
isabelle.control-bold.label=Control bold
isabelle.control-bold.shortcut=C+e RIGHT
-isabelle.control-isub.label=Control subscript
-isabelle.control-isub.shortcut=C+e DOWN
+isabelle.control-sub.label=Control subscript
+isabelle.control-sub.shortcut=C+e DOWN
isabelle.control-reset.label=Control reset
isabelle.control-reset.shortcut=C+e LEFT
isabelle.control-sup.label=Control superscript
--- a/src/Tools/jEdit/src/token_markup.scala Tue Aug 13 19:52:12 2013 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Tue Aug 13 20:34:46 2013 +0200
@@ -28,8 +28,7 @@
/* editing support for control symbols */
val is_control_style =
- Set(Symbol.sub_decoded, Symbol.sup_decoded,
- Symbol.isub_decoded, Symbol.isup_decoded, Symbol.bold_decoded)
+ Set(Symbol.sub_decoded, Symbol.sup_decoded, Symbol.bold_decoded)
def update_control_style(control: String, text: String): String =
{
@@ -161,8 +160,8 @@
{
// FIXME Symbol.bsub_decoded etc.
def control_style(sym: String): Option[Byte => Byte] =
- if (sym == Symbol.sub_decoded || sym == Symbol.isub_decoded) Some(subscript(_))
- else if (sym == Symbol.sup_decoded || sym == Symbol.isup_decoded) Some(superscript(_))
+ if (sym == Symbol.sub_decoded) Some(subscript(_))
+ else if (sym == Symbol.sup_decoded) Some(superscript(_))
else if (sym == Symbol.bold_decoded) Some(bold(_))
else None