1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Feb 06 20:03:42 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Feb 06 21:05:06 2013 +0100
     1.3 @@ -172,15 +172,20 @@
     1.4  
     1.5      val buffer = text_area.getBuffer
     1.6  
     1.7 -    val p = text_area.offsetToXY(range.start)
     1.8 -
     1.9      val end = buffer.getLength
    1.10      val stop = range.stop
    1.11 -    val (q, r) =
    1.12 -      if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
    1.13 -      else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
    1.14 -        (text_area.offsetToXY(stop - 1), char_width)
    1.15 -      else (text_area.offsetToXY(stop), 0)
    1.16 +
    1.17 +    val (p, q, r) =
    1.18 +      try {
    1.19 +        val p = text_area.offsetToXY(range.start)
    1.20 +        val (q, r) =
    1.21 +          if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
    1.22 +          else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
    1.23 +            (text_area.offsetToXY(stop - 1), char_width)
    1.24 +          else (text_area.offsetToXY(stop), 0)
    1.25 +        (p, q, r)
    1.26 +      }
    1.27 +      catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }
    1.28  
    1.29      if (p != null && q != null && p.x < q.x + r && p.y == q.y)
    1.30        Some(Gfx_Range(p.x, p.y, q.x + r - p.x))