src/Tools/jEdit/src/jedit_lib.scala
changeset 53183 018d71bee930
parent 53019 be9e94594b96
child 53226 9cf8e2263ca7
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Aug 24 17:39:18 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Aug 24 17:41:57 2013 +0200
     1.3 @@ -244,11 +244,20 @@
     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, false))
     1.8 -    gfx_range(text_area, range) match {
     1.9 -      case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
    1.10 -      case _ => None
    1.11 +    // coordinates wrt. inner painter component
    1.12 +    val painter = text_area.getPainter
    1.13 +    if (0 <= x && x < painter.getWidth && 0 <= y && y < painter.getHeight) {
    1.14 +      val offset = text_area.xyToOffset(x, y, false)
    1.15 +      if (offset >= 0) {
    1.16 +        val range = point_range(text_area.getBuffer, offset)
    1.17 +        gfx_range(text_area, range) match {
    1.18 +          case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
    1.19 +          case _ => None
    1.20 +        }
    1.21 +      }
    1.22 +      else None
    1.23      }
    1.24 +    else None
    1.25    }
    1.26  
    1.27