# HG changeset patch
# User wenzelm
# Date 1396120958 -3600
# Node ID f9ad26836516987c4a1059a980b6d422662c0e6b
# Parent  7e8c11011fdf411fd7655dd0bc6eb83a59e3f200
check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;

diff -r 7e8c11011fdf -r f9ad26836516 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 29 12:42:24 2014 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 29 20:22:38 2014 +0100
@@ -10,10 +10,11 @@
 
 import isabelle._
 
-import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor}
+import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor, MouseInfo}
 import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
   FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
 import java.awt.font.TextAttribute
+import javax.swing.SwingUtilities
 import java.text.AttributedString
 import java.util.ArrayList
 
@@ -180,6 +181,16 @@
     }
   }
 
+  private def mouse_inside_painter(): Boolean =
+    MouseInfo.getPointerInfo match {
+      case null => false
+      case info =>
+        val point = info.getLocation
+        val painter = text_area.getPainter
+        SwingUtilities.convertPointFromScreen(point, painter)
+        painter.contains(point)
+    }
+
   private val mouse_motion_listener = new MouseMotionAdapter {
     override def mouseDragged(evt: MouseEvent) {
       robust_body(()) {
@@ -213,23 +224,25 @@
         if (evt.getSource == text_area.getPainter) {
           Pretty_Tooltip.invoke(() =>
             robust_body(()) {
-              val rendering = get_rendering()
-              val snapshot = rendering.snapshot
-              if (!snapshot.is_outdated) {
-                JEdit_Lib.pixel_range(text_area, x, y) match {
-                  case None =>
-                  case Some(range) =>
-                    val result =
-                      if (control) rendering.tooltip(range)
-                      else rendering.tooltip_message(range)
-                    result match {
-                      case None =>
-                      case Some(tip) =>
-                        val painter = text_area.getPainter
-                        val loc = new Point(x, y + painter.getFontMetrics.getHeight / 2)
-                        val results = rendering.command_results(range)
-                        Pretty_Tooltip(view, painter, loc, rendering, results, tip)
-                    }
+              if (mouse_inside_painter()) {
+                val rendering = get_rendering()
+                val snapshot = rendering.snapshot
+                if (!snapshot.is_outdated) {
+                  JEdit_Lib.pixel_range(text_area, x, y) match {
+                    case None =>
+                    case Some(range) =>
+                      val result =
+                        if (control) rendering.tooltip(range)
+                        else rendering.tooltip_message(range)
+                      result match {
+                        case None =>
+                        case Some(tip) =>
+                          val painter = text_area.getPainter
+                          val loc = new Point(x, y + painter.getFontMetrics.getHeight / 2)
+                          val results = rendering.command_results(range)
+                          Pretty_Tooltip(view, painter, loc, rendering, results, tip)
+                      }
+                  }
                 }
               }
           })