# HG changeset patch # User wenzelm # Date 1376418945 -7200 # Node ID 5f4703de414066e330ad5f41ae76e5f9213771ea # Parent 11ebef554439002b7977c3bdf7921d67140f8317# Parent d0fa3f446b9d296ecd5e581b51b5fa161c38051e merged diff -r 11ebef554439 -r 5f4703de4140 NEWS --- 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 diff -r 11ebef554439 -r 5f4703de4140 etc/symbols --- 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 @@ \ 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 11ebef554439 -r 5f4703de4140 lib/texinputs/isabelle.sty --- 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} diff -r 11ebef554439 -r 5f4703de4140 src/HOL/Tools/Nitpick/nitpick_util.ML --- 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 diff -r 11ebef554439 -r 5f4703de4140 src/Pure/General/scan.scala --- 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)) ^^ diff -r 11ebef554439 -r 5f4703de4140 src/Pure/General/symbol.scala --- 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 diff -r 11ebef554439 -r 5f4703de4140 src/Pure/Thy/html.ML --- 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; diff -r 11ebef554439 -r 5f4703de4140 src/Pure/Thy/term_style.ML --- 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; diff -r 11ebef554439 -r 5f4703de4140 src/Tools/WWW_Find/html_unicode.ML --- 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 "" "") (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 11ebef554439 -r 5f4703de4140 src/Tools/jEdit/README.html --- 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 @@ sub =_ ⇩ sup =^ ⇧ - isup -_ ⇣ - isub -^ ⇡ bold -. ❙ diff -r 11ebef554439 -r 5f4703de4140 src/Tools/jEdit/src/actions.xml --- 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); - - - isabelle.jedit.Isabelle.control_isub(textArea); - - - - - isabelle.jedit.Isabelle.control_isup(textArea); - - isabelle.jedit.Isabelle.control_bold(textArea); diff -r 11ebef554439 -r 5f4703de4140 src/Tools/jEdit/src/isabelle.scala --- 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) } diff -r 11ebef554439 -r 5f4703de4140 src/Tools/jEdit/src/jEdit.props --- 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 diff -r 11ebef554439 -r 5f4703de4140 src/Tools/jEdit/src/jedit_lib.scala --- 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] = diff -r 11ebef554439 -r 5f4703de4140 src/Tools/jEdit/src/pretty_tooltip.scala --- 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) diff -r 11ebef554439 -r 5f4703de4140 src/Tools/jEdit/src/token_markup.scala --- 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