--- 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