--- a/NEWS Tue Aug 13 19:57:57 2013 +0200
+++ b/NEWS Tue Aug 13 20:35:45 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:57:57 2013 +0200
+++ b/etc/symbols Tue Aug 13 20:35:45 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:57:57 2013 +0200
+++ b/lib/texinputs/isabelle.sty Tue Aug 13 20:35:45 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:57:57 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Aug 13 20:35:45 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:57:57 2013 +0200
+++ b/src/Pure/General/scan.scala Tue Aug 13 20:35:45 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:57:57 2013 +0200
+++ b/src/Pure/General/symbol.scala Tue Aug 13 20:35:45 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:57:57 2013 +0200
+++ b/src/Pure/Thy/html.ML Tue Aug 13 20:35:45 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:57:57 2013 +0200
+++ b/src/Pure/Thy/term_style.ML Tue Aug 13 20:35:45 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:57:57 2013 +0200
+++ b/src/Tools/WWW_Find/html_unicode.ML Tue Aug 13 20:35:45 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:57:57 2013 +0200
+++ b/src/Tools/jEdit/README.html Tue Aug 13 20:35:45 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:57:57 2013 +0200
+++ b/src/Tools/jEdit/src/actions.xml Tue Aug 13 20:35:45 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:57:57 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Tue Aug 13 20:35:45 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:57:57 2013 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Tue Aug 13 20:35:45 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/jedit_lib.scala Tue Aug 13 19:57:57 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Tue Aug 13 20:35:45 2013 +0200
@@ -10,7 +10,7 @@
import isabelle._
import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
-import javax.swing.{Icon, ImageIcon}
+import javax.swing.{Icon, ImageIcon, JWindow}
import scala.annotation.tailrec
@@ -34,6 +34,36 @@
}
+ /* window geometry measurement */
+
+ private lazy val dummy_window = new JWindow
+
+ final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int)
+ {
+ def deco_width: Int = width - inner_width
+ def deco_height: Int = height - inner_height
+ }
+
+ def window_geometry(outer: Container, inner: Component): Window_Geometry =
+ {
+ Swing_Thread.require()
+
+ val old_content = dummy_window.getContentPane
+
+ dummy_window.setContentPane(outer)
+ dummy_window.pack
+ dummy_window.revalidate
+
+ val geometry =
+ Window_Geometry(
+ dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight)
+
+ dummy_window.setContentPane(old_content)
+
+ geometry
+ }
+
+
/* GUI components */
def get_parent(component: Component): Option[Container] =
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Tue Aug 13 19:57:57 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Tue Aug 13 20:35:45 2013 +0200
@@ -11,7 +11,7 @@
import java.awt.{Color, Point, BorderLayout, Dimension}
import java.awt.event.{FocusAdapter, FocusEvent}
-import javax.swing.{JWindow, JPanel, JComponent, PopupFactory}
+import javax.swing.{JPanel, JComponent, PopupFactory}
import javax.swing.border.LineBorder
import scala.swing.{FlowPanel, Label}
@@ -133,28 +133,6 @@
true
}
}
-
-
- /* auxiliary geometry measurement */
-
- private lazy val dummy_window = new JWindow
-
- private def decoration_size(tip: Pretty_Tooltip): (Int, Int) =
- {
- val old_content = dummy_window.getContentPane
-
- dummy_window.setContentPane(tip)
- dummy_window.pack
- dummy_window.revalidate
-
- val painter = tip.pretty_text_area.getPainter
- val w = dummy_window.getWidth - painter.getWidth
- val h = dummy_window.getHeight - painter.getHeight
-
- dummy_window.setContentPane(old_content)
-
- (w, h)
- }
}
@@ -253,10 +231,10 @@
XML.traverse_text(formatted)(0)(
(n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
- val (deco_width, deco_height) = Pretty_Tooltip.decoration_size(tip)
+ val geometry = JEdit_Lib.window_geometry(tip, tip.pretty_text_area.getPainter)
val bounds = rendering.tooltip_bounds
- val h1 = painter.getFontMetrics.getHeight * (lines + 1) + deco_height
+ val h1 = painter.getFontMetrics.getHeight * (lines + 1) + geometry.deco_height
val h2 = (screen_bounds.height * bounds).toInt
val h = h1 min h2
@@ -265,7 +243,7 @@
(0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) })
else margin
val w =
- ((metric.unit * (margin1 + metric.average)).round.toInt + deco_width) min
+ ((metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width) min
(screen_bounds.width * bounds).toInt
(w, h)
--- a/src/Tools/jEdit/src/token_markup.scala Tue Aug 13 19:57:57 2013 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Tue Aug 13 20:35:45 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