# HG changeset patch
# User wenzelm
# Date 1377358917 -7200
# Node ID 018d71bee930a21bb1c4474550650658259315fb
# Parent  61b983193dc111bfeb339a1040d292c828417bd3
strict checking of coordinates wrt. inner painter component;

diff -r 61b983193dc1 -r 018d71bee930 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Aug 24 17:39:18 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Aug 24 17:41:57 2013 +0200
@@ -244,11 +244,20 @@
 
   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, false))
-    gfx_range(text_area, range) match {
-      case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
-      case _ => None
+    // coordinates wrt. inner painter component
+    val painter = text_area.getPainter
+    if (0 <= x && x < painter.getWidth && 0 <= y && y < painter.getHeight) {
+      val offset = text_area.xyToOffset(x, y, false)
+      if (offset >= 0) {
+        val range = point_range(text_area.getBuffer, offset)
+        gfx_range(text_area, range) match {
+          case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
+          case _ => None
+        }
+      }
+      else None
     }
+    else None
   }