# HG changeset patch # User wenzelm # Date 1376418886 -7200 # Node ID d0fa3f446b9d296ecd5e581b51b5fa161c38051e # Parent afdabfeb5e940009e5a2f478786b06783cdaf91b discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end; document antiquotations: renamed term style "isub" to "sub"; diff -r afdabfeb5e94 -r d0fa3f446b9d NEWS --- 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 diff -r afdabfeb5e94 -r d0fa3f446b9d etc/symbols --- 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 @@ \ 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: =_) diff -r afdabfeb5e94 -r d0fa3f446b9d lib/texinputs/isabelle.sty --- 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} diff -r afdabfeb5e94 -r d0fa3f446b9d src/HOL/Tools/Nitpick/nitpick_util.ML --- 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 diff -r afdabfeb5e94 -r d0fa3f446b9d src/Pure/General/scan.scala --- 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)) ^^ diff -r afdabfeb5e94 -r d0fa3f446b9d src/Pure/General/symbol.scala --- 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 diff -r afdabfeb5e94 -r d0fa3f446b9d src/Pure/Thy/html.ML --- 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; diff -r afdabfeb5e94 -r d0fa3f446b9d src/Pure/Thy/term_style.ML --- 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; diff -r afdabfeb5e94 -r d0fa3f446b9d src/Tools/WWW_Find/html_unicode.ML --- 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 "" "") (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 [] = []; diff -r afdabfeb5e94 -r d0fa3f446b9d src/Tools/jEdit/README.html --- 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 @@ sub =_ ⇩ sup =^ ⇧ - isup -_ ⇣ - isub -^ ⇡ bold -. ❙ diff -r afdabfeb5e94 -r d0fa3f446b9d src/Tools/jEdit/src/actions.xml --- 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); - - - isabelle.jedit.Isabelle.control_isub(textArea); - - - - - isabelle.jedit.Isabelle.control_isup(textArea); - - isabelle.jedit.Isabelle.control_bold(textArea); diff -r afdabfeb5e94 -r d0fa3f446b9d src/Tools/jEdit/src/isabelle.scala --- 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) } diff -r afdabfeb5e94 -r d0fa3f446b9d src/Tools/jEdit/src/jEdit.props --- 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 diff -r afdabfeb5e94 -r d0fa3f446b9d src/Tools/jEdit/src/token_markup.scala --- 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