src/Tools/jEdit/src/rich_text_area.scala

--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Oct 04 13:56:32 2012 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Oct 04 18:28:31 2012 +0200
@@ -10,12 +10,14 @@
 
 import isabelle._
 
-import java.awt.{Graphics2D, Shape, Window, Color}
+import java.awt.{Graphics2D, Shape, Window, Color, Point, BorderLayout}
 import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
   FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
 import java.awt.font.TextAttribute
 import java.text.AttributedString
 import java.util.ArrayList
+import javax.swing.{SwingUtilities, JWindow, JPanel}
+import javax.swing.border.LineBorder
 
 import org.gjt.sp.util.Log
 import org.gjt.sp.jedit.{OperatingSystem, Debug, View}
@@ -198,12 +200,43 @@
     {
       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) {
+            val point = {
+              val painter = text_area.getPainter
+              val bounds = painter.getBounds()
+              val point = new Point(bounds.x + x, bounds.y + painter.getFontMetrics.getHeight + y)
+              SwingUtilities.convertPointToScreen(point, painter)
+              point
+            }
+
+            val tooltip_text = new Pretty_Text_Area(view)
+            tooltip_text.resize(Isabelle.font_family(), Isabelle.font_size().round) // FIXME tooltip_scale
+            tooltip_text.update(snapshot, tip)
+
+            val window = new JWindow(view) {
+              addWindowFocusListener(new WindowAdapter {
+                override def windowLostFocus(e: WindowEvent) { dispose() }
+              })
+              setContentPane(new JPanel(new BorderLayout) {
+                override def getFocusTraversalKeysEnabled(): Boolean = false
+              })
+              getRootPane.setBorder(new LineBorder(Color.BLACK))
+
+              add(tooltip_text)
+              setSize(300, 100)
+              setLocation(point.x, point.y)
+              setVisible(true)
+            }
+          }
+        }
+        null
       }
     }
   }