# HG changeset patch
# User wenzelm
# Date 1353245070 -3600
# Node ID 88b971fca902944b5895731d82a4fcd77d1c4ffb
# Parent  8cde6f1a0106a21fd94a46837264226bc1721e2e
more accurate pixel_range -- do not round offset here;

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