# HG changeset patch
# User wenzelm
# Date 1398344386 -7200
# Node ID 60ad80f5cb622321a7dd1f390e6ad49a0aaa6512
# Parent  e0655270d3f35758f3a378add3958690f6df32c0
further robustification wrt. unclear ranges;

diff -r e0655270d3f3 -r 60ad80f5cb62 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Apr 24 14:51:41 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Apr 24 14:59:46 2014 +0200
@@ -215,9 +215,12 @@
     val buffer = text_area.getBuffer
     buffer_range(buffer).try_restrict(range) match {
       case Some(range1) if !range1.is_singularity =>
-        text_area.invalidateLineRange(
-          buffer.getLineOfOffset(range1.start),
-          buffer.getLineOfOffset(range1.stop))
+        try {
+          text_area.invalidateLineRange(
+            buffer.getLineOfOffset(range1.start),
+            buffer.getLineOfOffset(range1.stop))
+        }
+        catch { case _: ArrayIndexOutOfBoundsException => }
       case _ =>
     }
   }