--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Oct 05 10:57:03 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Oct 05 14:51:33 2012 +0200
@@ -708,8 +708,10 @@
lemma (in real_vector) span_subspace: "A \<subseteq> B \<Longrightarrow> B \<le> span A \<Longrightarrow> subspace B \<Longrightarrow> span A = B"
by (metis order_antisym span_def hull_minimal)
-lemma (in real_vector) span_induct': assumes SP: "\<forall>x \<in> S. P x"
- and P: "subspace {x. P x}" shows "\<forall>x \<in> span S. P x"
+lemma (in real_vector) span_induct':
+ assumes SP: "\<forall>x \<in> S. P x"
+ and P: "subspace {x. P x}"
+ shows "\<forall>x \<in> span S. P x"
using span_induct SP P by blast
inductive_set (in real_vector) span_induct_alt_help for S:: "'a set"
@@ -842,7 +844,8 @@
ultimately show "subspace ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
by (rule subspace_linear_image)
next
- fix T assume "A \<union> B \<subseteq> T" and "subspace T"
+ fix T
+ assume "A \<union> B \<subseteq> T" and "subspace T"
then show "(\<lambda>(a, b). a + b) ` (span A \<times> span B) \<subseteq> T"
by (auto intro!: subspace_add elim: span_induct)
qed
@@ -885,7 +888,8 @@
text {* Hence some "reversal" results. *}
lemma in_span_insert:
- assumes a: "a \<in> span (insert b S)" and na: "a \<notin> span S"
+ assumes a: "a \<in> span (insert b S)"
+ and na: "a \<notin> span S"
shows "b \<in> span (insert a S)"
proof -
from span_breakdown[of b "insert b S" a, OF insertI1 a]
@@ -1073,7 +1077,8 @@
shows "span S = {y. \<exists>u. setsum (\<lambda>v. u v *\<^sub>R v) S = y}"
(is "_ = ?rhs")
proof -
- { fix y assume y: "y \<in> span S"
+ { fix y
+ assume y: "y \<in> span S"
from y obtain S' u where fS': "finite S'" and SS': "S' \<subseteq> S" and
u: "setsum (\<lambda>v. u v *\<^sub>R v) S' = y" unfolding span_explicit by blast
let ?u = "\<lambda>x. if x \<in> S' then u x else 0"
@@ -1135,7 +1140,8 @@
by blast
lemma spanning_subset_independent:
- assumes BA: "B \<subseteq> A" and iA: "independent A"
+ assumes BA: "B \<subseteq> A"
+ and iA: "independent A"
and AsB: "A \<subseteq> span B"
shows "A = B"
proof
@@ -1162,8 +1168,9 @@
text {* The general case of the Exchange Lemma, the key to what follows. *}
lemma exchange_lemma:
- assumes f:"finite t" and i: "independent s"
- and sp:"s \<subseteq> span t"
+ assumes f:"finite t"
+ and i: "independent s"
+ and sp: "s \<subseteq> span t"
shows "\<exists>t'. (card t' = card t) \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
using f i sp
proof (induct "card (t - s)" arbitrary: s t rule: less_induct)
@@ -1177,11 +1184,12 @@
done }
moreover
{ assume st: "t \<subseteq> s"
-
from spanning_subset_independent[OF st s sp]
- st ft span_mono[OF st] have ?ths apply - apply (rule exI[where x=t])
- apply (auto intro: span_superset)
- done }
+ st ft span_mono[OF st] have ?ths
+ apply -
+ apply (rule exI[where x=t])
+ apply (auto intro: span_superset)
+ done }
moreover
{ assume st: "\<not> s \<subseteq> t" "\<not> t \<subseteq> s"
from st(2) obtain b where b: "b \<in> t" "b \<notin> s" by blast
@@ -1276,8 +1284,7 @@
apply (simp add: inner_setsum_right dot_basis)
done
-lemma (in euclidean_space) range_basis:
- "range basis = insert 0 (basis ` {..<DIM('a)})"
+lemma (in euclidean_space) range_basis: "range basis = insert 0 (basis ` {..<DIM('a)})"
proof -
have *: "UNIV = {..<DIM('a)} \<union> {DIM('a)..}" by auto
show ?thesis unfolding * image_Un basis_finite by auto
@@ -1508,7 +1515,8 @@
apply (rule setsum_norm_le)
using fN fM
apply simp
- apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] field_simps simp del: scaleR_scaleR)
+ apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]
+ field_simps simp del: scaleR_scaleR)
apply (rule mult_mono)
apply (auto simp add: zero_le_mult_iff component_le_norm)
apply (rule mult_mono)
@@ -1930,7 +1938,8 @@
apply (clarsimp simp add: inner_add inner_setsum_left)
apply (rule setsum_0', rule ballI)
unfolding inner_commute
- apply (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])
+ apply (auto simp add: x field_simps
+ intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])
done }
then show "\<forall>x \<in> B. ?a \<bullet> x = 0" by blast
qed
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Oct 05 10:57:03 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Oct 05 14:51:33 2012 +0200
@@ -28,12 +28,14 @@
lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)"
proof-
- {assume "T1=T2" hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp}
+ { assume "T1=T2"
+ hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp }
moreover
- {assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
+ { assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
hence "openin T1 = openin T2" by (simp add: fun_eq_iff)
hence "topology (openin T1) = topology (openin T2)" by simp
- hence "T1 = T2" unfolding openin_inverse .}
+ hence "T1 = T2" unfolding openin_inverse .
+ }
ultimately show ?thesis by blast
qed
@@ -66,9 +68,11 @@
lemma openin_topspace[intro, simp]: "openin U (topspace U)" by (simp add: openin_Union topspace_def)
-lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)" (is "?lhs \<longleftrightarrow> ?rhs")
+lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)"
+ (is "?lhs \<longleftrightarrow> ?rhs")
proof
- assume ?lhs then show ?rhs by auto
+ assume ?lhs
+ then show ?rhs by auto
next
assume H: ?rhs
let ?t = "\<Union>{T. openin U T \<and> T \<subseteq> S}"
@@ -77,6 +81,7 @@
finally show "openin U S" .
qed
+
subsubsection {* Closed sets *}
definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
@@ -167,9 +172,11 @@
apply (rule iffI, clarify)
apply (frule openin_subset[of U]) apply blast
apply (rule exI[where x="topspace U"])
- by auto
-
-lemma subtopology_superset: assumes UV: "topspace U \<subseteq> V"
+ apply auto
+ done
+
+lemma subtopology_superset:
+ assumes UV: "topspace U \<subseteq> V"
shows "subtopology U V = U"
proof-
{fix S
--- a/src/Tools/jEdit/etc/options Fri Oct 05 10:57:03 2012 +0200
+++ b/src/Tools/jEdit/etc/options Fri Oct 05 14:51:33 2012 +0200
@@ -9,8 +9,8 @@
option jedit_font_scale : real = 1.0
-- "scale factor of add-on panels wrt. main text area"
-option jedit_tooltip_font_size : int = 10
- -- "tooltip font size (according to HTML)"
+option jedit_tooltip_font_scale : real = 0.85
+ -- "scale factor of tooltips wrt. main text area"
option jedit_tooltip_margin : int = 60
-- "margin for tooltip pretty-printing"
@@ -30,6 +30,7 @@
option running_color : string = "610061FF"
option running1_color : string = "61006164"
option light_color : string = "F0F0F0FF"
+option tooltip_color : string = "FFFFE9FF"
option writeln_color : string = "C0C0C0FF"
option warning_color : string = "FF8C00FF"
option error_color : string = "B22222FF"
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Oct 05 10:57:03 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Fri Oct 05 14:51:33 2012 +0200
@@ -26,6 +26,7 @@
"src/output_dockable.scala"
"src/plugin.scala"
"src/pretty_text_area.scala"
+ "src/pretty_tooltip.scala"
"src/protocol_dockable.scala"
"src/raw_output_dockable.scala"
"src/readme_dockable.scala"
--- a/src/Tools/jEdit/src/isabelle_logic.scala Fri Oct 05 10:57:03 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Fri Oct 05 14:51:33 2012 +0200
@@ -56,7 +56,7 @@
component.listenTo(component.selection)
component.reactions += { case SelectionChanged(_) => component.save() }
}
- component.tooltip = Isabelle.tooltip(Isabelle.options.value.check_name(opt_name).print_default)
+ component.tooltip = Isabelle.options.value.check_name(opt_name).print_default
component
}
--- a/src/Tools/jEdit/src/isabelle_options.scala Fri Oct 05 10:57:03 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala Fri Oct 05 14:51:33 2012 +0200
@@ -42,7 +42,7 @@
// FIXME avoid hard-wired stuff
private val relevant_options =
Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_text_overview",
- "jedit_tooltip_font_size", "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay",
+ "jedit_tooltip_font_scale", "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay",
"editor_load_delay", "editor_input_delay", "editor_output_delay",
"editor_update_delay", "editor_reparse_limit")
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Fri Oct 05 10:57:03 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Fri Oct 05 14:51:33 2012 +0200
@@ -112,6 +112,7 @@
val running_color = color_value("running_color")
val running1_color = color_value("running1_color")
val light_color = color_value("light_color")
+ val tooltip_color = color_value("tooltip_color")
val writeln_color = color_value("writeln_color")
val warning_color = color_value("warning_color")
val error_color = color_value("error_color")
@@ -259,26 +260,23 @@
}
- private def tooltip_text(msg: XML.Tree): String =
- Pretty.string_of(List(msg), margin = options.int("jedit_tooltip_margin"))
-
- def tooltip_message(range: Text.Range): Option[String] =
+ def tooltip_message(range: Text.Range): XML.Body =
{
val msgs =
- snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
+ snapshot.cumulate_markup[SortedMap[Long, XML.Tree]](range, SortedMap.empty,
Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR,
Isabelle_Markup.BAD)),
{
- case (msgs, Text.Info(_, msg @
- XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
- if markup == Isabelle_Markup.WRITELN ||
- markup == Isabelle_Markup.WARNING ||
- markup == Isabelle_Markup.ERROR =>
- msgs + (serial -> tooltip_text(msg))
+ case (msgs, Text.Info(_,
+ XML.Elem(Markup(name, props @ Isabelle_Markup.Serial(serial)), body)))
+ if name == Isabelle_Markup.WRITELN ||
+ name == Isabelle_Markup.WARNING ||
+ name == Isabelle_Markup.ERROR =>
+ msgs + (serial -> XML.Elem(Markup(Isabelle_Markup.message(name), props), body))
case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Isabelle_Markup.BAD, _), body)))
- if !body.isEmpty => msgs + (Document.new_id() -> tooltip_text(msg))
+ if !body.isEmpty => msgs + (Document.new_id() -> msg)
}).toList.flatMap(_.info)
- if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2)))
+ Library.separate(Pretty.Separator, msgs.iterator.map(_._2).toList)
}
@@ -302,38 +300,37 @@
Set(Isabelle_Markup.ENTITY, Isabelle_Markup.SORTING, Isabelle_Markup.TYPING,
Isabelle_Markup.ML_TYPING, Isabelle_Markup.PATH) ++ tooltips.keys
- private def string_of_typing(kind: String, body: XML.Body): String =
- Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
- margin = options.int("jedit_tooltip_margin"))
+ private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
+ Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
- def tooltip(range: Text.Range): Option[String] =
+ def tooltip(range: Text.Range): XML.Body =
{
- def add(prev: Text.Info[List[(Boolean, String)]], r: Text.Range, p: (Boolean, String)) =
+ def add(prev: Text.Info[List[(Boolean, XML.Tree)]], r: Text.Range, p: (Boolean, XML.Tree)) =
if (prev.range == r) Text.Info(r, p :: prev.info) else Text.Info(r, List(p))
val tips =
- snapshot.cumulate_markup[Text.Info[(List[(Boolean, String)])]](
+ snapshot.cumulate_markup[Text.Info[(List[(Boolean, XML.Tree)])]](
range, Text.Info(range, Nil), Some(tooltip_elements),
{
case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) =>
val kind1 = space_explode('_', kind).mkString(" ")
- add(prev, r, (true, kind1 + " " + quote(name)))
+ add(prev, r, (true, XML.Text(kind1 + " " + quote(name))))
case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Path(name), _)))
if Path.is_ok(name) =>
val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
- add(prev, r, (true, "file " + quote(jedit_file)))
+ add(prev, r, (true, XML.Text("file " + quote(jedit_file))))
case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
if name == Isabelle_Markup.SORTING || name == Isabelle_Markup.TYPING =>
- add(prev, r, (true, string_of_typing("::", body)))
+ add(prev, r, (true, pretty_typing("::", body)))
case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) =>
- add(prev, r, (false, string_of_typing("ML:", body)))
+ add(prev, r, (false, pretty_typing("ML:", body)))
case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
- if tooltips.isDefinedAt(name) => add(prev, r, (true, tooltips(name)))
+ if tooltips.isDefinedAt(name) => add(prev, r, (true, XML.Text(tooltips(name))))
}).toList.flatMap(_.info.info)
val all_tips =
(tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
- if (all_tips.isEmpty) None else Some(cat_lines(all_tips))
+ Library.separate(Pretty.FBreak, all_tips.toList)
}
--- a/src/Tools/jEdit/src/jedit_lib.scala Fri Oct 05 10:57:03 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Fri Oct 05 14:51:33 2012 +0200
@@ -9,6 +9,9 @@
import isabelle._
+import java.awt.{Component, Container, Frame, Window}
+
+import scala.annotation.tailrec
import org.gjt.sp.jedit.{jEdit, Buffer, View}
import org.gjt.sp.jedit.buffer.JEditBuffer
@@ -17,6 +20,33 @@
object JEdit_Lib
{
+ /* GUI components */
+
+ def get_parent(component: Component): Option[Container] =
+ component.getParent match {
+ case null => None
+ case parent => Some(parent)
+ }
+
+ def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
+ private var next_elem = get_parent(component)
+ def hasNext(): Boolean = next_elem.isDefined
+ def next(): Container =
+ next_elem match {
+ case Some(parent) =>
+ next_elem = get_parent(parent)
+ parent
+ case None => Iterator.empty.next()
+ }
+ }
+
+ def parent_window(component: Component): Option[Window] =
+ ancestors(component).find(_.isInstanceOf[Window]).map(_.asInstanceOf[Window])
+
+ def parent_frame(component: Component): Option[Frame] =
+ ancestors(component).find(_.isInstanceOf[Frame]).map(_.asInstanceOf[Frame])
+
+
/* buffers */
def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
--- a/src/Tools/jEdit/src/jedit_options.scala Fri Oct 05 10:57:03 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala Fri Oct 05 14:51:33 2012 +0200
@@ -44,7 +44,7 @@
def load = button.setSelectedColor(Color_Value(string(opt_name)))
def save = string(opt_name) = Color_Value.print(button.getSelectedColor)
}
- component.tooltip = Isabelle.tooltip(opt.print_default)
+ component.tooltip = opt.print_default
component
}
@@ -91,7 +91,7 @@
text_area
}
component.load()
- component.tooltip = Isabelle.tooltip(opt.print_default)
+ component.tooltip = opt.print_default
component
}
--- a/src/Tools/jEdit/src/output_dockable.scala Fri Oct 05 10:57:03 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Fri Oct 05 14:51:33 2012 +0200
@@ -48,7 +48,7 @@
Swing_Thread.require()
pretty_text_area.resize(Isabelle.font_family(),
- scala.math.round(Isabelle.font_size() * zoom_factor / 100))
+ scala.math.round(Isabelle.font_size("jedit_font_scale") * zoom_factor / 100))
}
private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
--- a/src/Tools/jEdit/src/plugin.scala Fri Oct 05 10:57:03 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Fri Oct 05 14:51:33 2012 +0200
@@ -51,16 +51,11 @@
def font_family(): String = jEdit.getProperty("view.font")
- def font_size(): Float =
- (jEdit.getIntegerProperty("view.fontsize", 16) * options.real("jedit_font_scale")).toFloat
+ def font_size(scale: String): Float =
+ (jEdit.getIntegerProperty("view.fontsize", 16) * options.real(scale)).toFloat
- /* tooltip markup */
-
- def tooltip(text: String): String =
- "<html><pre style=\"font-family: " + font_family() + "; font-size: " +
- options.int("jedit_tooltip_font_size").toString + "px; \">" + // FIXME proper scaling (!?)
- HTML.encode(text) + "</pre></html>"
+ /* tooltip delay */
private val tooltip_lb = Time.seconds(0.5)
private val tooltip_ub = Time.seconds(60.0)
--- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Oct 05 10:57:03 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Oct 05 14:51:33 2012 +0200
@@ -40,8 +40,6 @@
val version0 = base_snapshot.version
val nodes0 = version0.nodes
- assert(nodes0(node_name).commands.isEmpty)
-
val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
val version1 = Document.Version.make(version0.syntax, nodes1)
val state1 =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Fri Oct 05 14:51:33 2012 +0200
@@ -0,0 +1,95 @@
+/* Title: Tools/jEdit/src/pretty_tooltip.scala
+ Author: Makarius
+
+Enhanced tooltip window based on Pretty_Text_Area.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.{Toolkit, Color, Point, BorderLayout, Window}
+import java.awt.event.{ActionListener, ActionEvent, KeyEvent, WindowEvent, WindowAdapter}
+import javax.swing.{SwingUtilities, JWindow, JPanel, JComponent, KeyStroke}
+import javax.swing.border.LineBorder
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.textarea.TextArea
+
+
+class Pretty_Tooltip(
+ view: View,
+ text_area: TextArea,
+ rendering: Isabelle_Rendering,
+ mouse_x: Int, mouse_y: Int, body: XML.Body)
+ extends JWindow(JEdit_Lib.parent_window(text_area) getOrElse view)
+{
+ window =>
+
+ window.addWindowFocusListener(new WindowAdapter {
+ override def windowLostFocus(e: WindowEvent) {
+ if (!Window.getWindows.exists(w =>
+ w.isDisplayable && JEdit_Lib.ancestors(w).exists(_ == window)))
+ window.dispose()
+ }
+ })
+
+ window.setContentPane(new JPanel(new BorderLayout) {
+ private val action_listener = new ActionListener {
+ def actionPerformed(e: ActionEvent) {
+ e.getActionCommand match {
+ case "close" =>
+ window.dispose()
+ JEdit_Lib.ancestors(window) foreach {
+ case c: Pretty_Tooltip => c.dispose
+ case _ =>
+ }
+ case _ =>
+ }
+ }
+ }
+ registerKeyboardAction(action_listener, "close",
+ KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
+
+ override def getFocusTraversalKeysEnabled(): Boolean = false
+ })
+ window.getRootPane.setBorder(new LineBorder(Color.BLACK))
+
+ val pretty_text_area = new Pretty_Text_Area(view)
+ pretty_text_area.getPainter.setBackground(rendering.tooltip_color)
+ pretty_text_area.resize(
+ Isabelle.font_family(), Isabelle.font_size("jedit_tooltip_font_scale").round)
+ pretty_text_area.update(rendering.snapshot, body)
+
+ window.add(pretty_text_area)
+
+ {
+ val font_metrics = pretty_text_area.getPainter.getFontMetrics
+ val margin = Isabelle.options.int("jedit_tooltip_margin") // FIXME via rendering?!
+ val lines = // FIXME avoid redundant formatting
+ XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(font_metrics)))(0)(
+ (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
+
+ val screen = Toolkit.getDefaultToolkit.getScreenSize
+ val w = (font_metrics.charWidth(Pretty.spc) * margin) min (screen.width / 2)
+ val h = (font_metrics.getHeight * (lines + 2)) min (screen.height / 2)
+ window.setSize(w, h)
+ }
+
+ {
+ val container = text_area.getPainter
+ val font_metrics = container.getFontMetrics
+ val point = new Point(mouse_x, mouse_y + font_metrics.getHeight / 2)
+ SwingUtilities.convertPointToScreen(point, container)
+
+ val screen = Toolkit.getDefaultToolkit.getScreenSize
+ val x = point.x min (screen.width - window.getWidth)
+ val y = point.y min (screen.height - window.getHeight)
+ window.setLocation(x, y)
+ }
+
+ window.setVisible(true)
+ pretty_text_area.refresh() // FIXME avoid redundant formatting
+}
+
--- a/src/Tools/jEdit/src/rich_text_area.scala Fri Oct 05 10:57:03 2012 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Oct 05 14:51:33 2012 +0200
@@ -10,7 +10,7 @@
import isabelle._
-import java.awt.{Graphics2D, Shape, Window, Color}
+import java.awt.{Graphics2D, Shape, Window, Color, Point}
import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
import java.awt.font.TextAttribute
@@ -198,12 +198,16 @@
{
robust_body(null: String) {
val rendering = get_rendering()
- val offset = text_area.xyToOffset(x, y)
- val range = Text.Range(offset, offset + 1)
- val tip =
- if (control) rendering.tooltip(range)
- else rendering.tooltip_message(range)
- tip.map(Isabelle.tooltip(_)) getOrElse null
+ val snapshot = rendering.snapshot
+ if (!snapshot.is_outdated) {
+ val offset = text_area.xyToOffset(x, y)
+ val range = Text.Range(offset, offset + 1)
+ val tip =
+ if (control) rendering.tooltip(range)
+ else rendering.tooltip_message(range)
+ if (!tip.isEmpty) new Pretty_Tooltip(view, text_area, rendering, x, y, tip)
+ }
+ null
}
}
}