src/Tools/jEdit/src/jedit_lib.scala
changeset 56699 60ad80f5cb62
parent 56662 f373fb77e0a4
child 56774 2d39c313f39e
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Apr 24 14:51:41 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Apr 24 14:59:46 2014 +0200
     1.3 @@ -215,9 +215,12 @@
     1.4      val buffer = text_area.getBuffer
     1.5      buffer_range(buffer).try_restrict(range) match {
     1.6        case Some(range1) if !range1.is_singularity =>
     1.7 -        text_area.invalidateLineRange(
     1.8 -          buffer.getLineOfOffset(range1.start),
     1.9 -          buffer.getLineOfOffset(range1.stop))
    1.10 +        try {
    1.11 +          text_area.invalidateLineRange(
    1.12 +            buffer.getLineOfOffset(range1.start),
    1.13 +            buffer.getLineOfOffset(range1.stop))
    1.14 +        }
    1.15 +        catch { case _: ArrayIndexOutOfBoundsException => }
    1.16        case _ =>
    1.17      }
    1.18    }