# HG changeset patch
# User wenzelm
# Date 1349441493 -7200
# Node ID 519cf2ac6c0ead02e3fce772932422f1f3ac1f11
# Parent  6279490e043873971d8710ad10db56af2365a502# Parent  a1bd8fe5131bd47dd89401fa1f0629c85c99d4d5
merged

diff -r 6279490e0438 -r 519cf2ac6c0e src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- 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
diff -r 6279490e0438 -r 519cf2ac6c0e src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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
diff -r 6279490e0438 -r 519cf2ac6c0e src/Tools/jEdit/etc/options
--- 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"
diff -r 6279490e0438 -r 519cf2ac6c0e src/Tools/jEdit/lib/Tools/jedit
--- 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"
diff -r 6279490e0438 -r 519cf2ac6c0e src/Tools/jEdit/src/isabelle_logic.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
   }
 
diff -r 6279490e0438 -r 519cf2ac6c0e src/Tools/jEdit/src/isabelle_options.scala
--- 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")
 
diff -r 6279490e0438 -r 519cf2ac6c0e src/Tools/jEdit/src/isabelle_rendering.scala
--- 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)
   }
 
 
diff -r 6279490e0438 -r 519cf2ac6c0e src/Tools/jEdit/src/jedit_lib.scala
--- 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 =
diff -r 6279490e0438 -r 519cf2ac6c0e src/Tools/jEdit/src/jedit_options.scala
--- 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
   }
 
diff -r 6279490e0438 -r 519cf2ac6c0e src/Tools/jEdit/src/output_dockable.scala
--- 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]])
diff -r 6279490e0438 -r 519cf2ac6c0e src/Tools/jEdit/src/plugin.scala
--- 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)
diff -r 6279490e0438 -r 519cf2ac6c0e src/Tools/jEdit/src/pretty_text_area.scala
--- 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 =
diff -r 6279490e0438 -r 519cf2ac6c0e src/Tools/jEdit/src/pretty_tooltip.scala
--- /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
+}
+
diff -r 6279490e0438 -r 519cf2ac6c0e src/Tools/jEdit/src/rich_text_area.scala
--- 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
       }
     }
   }