diff -r 8cde6f1a0106 -r 88b971fca902 src/Tools/jEdit/src/jedit_lib.scala --- 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