further robustification wrt. unclear ranges;
authorwenzelm
Thu Apr 24 14:59:46 2014 +0200 (2014-04-24)
changeset 5669960ad80f5cb62
parent 56698 e0655270d3f3
child 56700 c84bf6f63dfe
further robustification wrt. unclear ranges;
src/Tools/jEdit/src/jedit_lib.scala
     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    }