more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;

--- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 19 21:19:06 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 19 21:52:45 2012 +0200
@@ -168,5 +168,17 @@
       Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
     else None
   }
+
+
+  /* pixel range */
+
+  def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
+  {
+    val range = point_range(text_area.getBuffer, text_area.xyToOffset(x, y))
+    gfx_range(text_area, range) match {
+      case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
+      case _ => None
+    }
+  }
 }
 

--- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Oct 19 21:19:06 2012 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Oct 19 21:52:45 2012 +0200
@@ -173,14 +173,16 @@
 
         if ((control || hovering) && !buffer.isLoading) {
           JEdit_Lib.buffer_lock(buffer) {
-            val rendering = get_rendering()
-            val mouse_offset = text_area.xyToOffset(e.getX(), e.getY())
-            val mouse_range = JEdit_Lib.point_range(buffer, mouse_offset)
-            for ((area, require_control) <- active_areas)
-            {
-              if (control == require_control)
-                area.update_rendering(rendering, mouse_range)
-              else area.reset
+            JEdit_Lib.pixel_range(text_area, e.getX(), e.getY()) match {
+              case None =>
+              case Some(range) =>
+                val rendering = get_rendering()
+                for ((area, require_control) <- active_areas)
+                {
+                  if (control == require_control)
+                    area.update_rendering(rendering, range)
+                  else area.reset
+                }
             }
           }
         }
@@ -200,15 +202,17 @@
         val rendering = get_rendering()
         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 painter = text_area.getPainter
-            val y1 = y + painter.getFontMetrics.getHeight / 2
-            new Pretty_Tooltip(view, painter, rendering, x, y1, tip)
+          JEdit_Lib.pixel_range(text_area, x, y) match {
+            case None =>
+            case Some(range) =>
+              val tip =
+                if (control) rendering.tooltip(range)
+                else rendering.tooltip_message(range)
+              if (!tip.isEmpty) {
+                val painter = text_area.getPainter
+                val y1 = y + painter.getFontMetrics.getHeight / 2
+                new Pretty_Tooltip(view, painter, rendering, x, y1, tip)
+              }
           }
         }
         null