src/Tools/jEdit/src/jedit_lib.scala
changeset 50116 88b971fca902
parent 50115 8cde6f1a0106
child 50186 f83cab68c788
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 18 13:52:54 2012 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 18 14:24:30 2012 +0100
@@ -174,7 +174,7 @@
 
   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))
+    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