more accurate pixel_range -- do not round offset here;
authorwenzelm
Sun Nov 18 14:24:30 2012 +0100 (2012-11-18)
changeset 5011688b971fca902
parent 50115 8cde6f1a0106
child 50117 32755e357a51
more accurate pixel_range -- do not round offset here;
src/Tools/jEdit/src/jedit_lib.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 18 13:52:54 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 18 14:24:30 2012 +0100
     1.3 @@ -174,7 +174,7 @@
     1.4  
     1.5    def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
     1.6    {
     1.7 -    val range = point_range(text_area.getBuffer, text_area.xyToOffset(x, y))
     1.8 +    val range = point_range(text_area.getBuffer, text_area.xyToOffset(x, y, false))
     1.9      gfx_range(text_area, range) match {
    1.10        case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
    1.11        case _ => None