# HG changeset patch
# User wenzelm
# Date 1349374480 -7200
# Node ID 696e91c0bc801411d7a6dd5c0bc74d3825a8dda9
# Parent  e2762f962042c6323acee1be5ca7d170fdc6398f
separate module Pretty_Tooltip;

diff -r e2762f962042 -r 696e91c0bc80 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Thu Oct 04 19:31:50 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Oct 04 20:14:40 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 e2762f962042 -r 696e91c0bc80 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	Thu Oct 04 20:14:40 2012 +0200
@@ -0,0 +1,55 @@
+/*  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.{Color, Point, BorderLayout}
+import java.awt.event.{WindowEvent, WindowAdapter}
+import javax.swing.{SwingUtilities, JWindow, JPanel}
+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,
+  x: Int, y: Int, body: XML.Body) extends JWindow(view)
+{
+  private val painter = text_area.getPainter
+  private val fm = painter.getFontMetrics
+
+  private val point = {
+    val bounds = painter.getBounds()
+    val point = new Point(bounds.x + x, bounds.y + fm.getHeight + y)
+    SwingUtilities.convertPointToScreen(point, painter)
+    point
+  }
+
+  val pretty_text_area = new Pretty_Text_Area(view)
+  pretty_text_area.resize(
+    Isabelle.font_family(), Isabelle.font_size("jedit_tooltip_font_scale").round)
+  pretty_text_area.update(rendering.snapshot, body)
+
+  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(pretty_text_area)
+  setSize(fm.charWidth(Pretty.spc) * Isabelle.options.int("jedit_tooltip_margin"), 100)
+  setLocation(point.x, point.y)
+  setVisible(true)
+}
+
diff -r e2762f962042 -r 696e91c0bc80 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Oct 04 19:31:50 2012 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Oct 04 20:14:40 2012 +0200
@@ -10,14 +10,12 @@
 
 import isabelle._
 
-import java.awt.{Graphics2D, Shape, Window, Color, Point, BorderLayout}
+import java.awt.{Graphics2D, Shape, Window, Color, Point}
 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}
@@ -202,43 +200,12 @@
         val rendering = get_rendering()
         val snapshot = rendering.snapshot
         if (!snapshot.is_outdated) {
-          val painter = text_area.getPainter
-          val fm = painter.getFontMetrics
-
           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 bounds = painter.getBounds()
-              val point = new Point(bounds.x + x, bounds.y + fm.getHeight + y)
-              SwingUtilities.convertPointToScreen(point, painter)
-              point
-            }
-
-            val tooltip_text = new Pretty_Text_Area(view)
-            tooltip_text.resize(Isabelle.font_family(),
-              Isabelle.font_size("jedit_tooltip_font_scale").round)
-
-            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(fm.charWidth(Pretty.spc) * Isabelle.options.int("jedit_tooltip_margin"), 100)
-              setLocation(point.x, point.y)
-              setVisible(true)
-            }
-          }
+          if (!tip.isEmpty) new Pretty_Tooltip(view, text_area, rendering, x, y, tip)
         }
         null
       }