# HG changeset patch
# User wenzelm
# Date 1285698178 -7200
# Node ID 8c312f0642237cc0a6e60c46d195ab9bec9134b3
# Parent  e19cece7d18a975a442548d291e9df75747ac682
more defensive overview.paintComponent: avoid potential crash due to buffer change while painting;

diff -r e19cece7d18a -r 8c312f064223 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 28 18:51:10 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 28 20:22:58 2010 +0200
@@ -364,14 +364,24 @@
     {
       super.paintComponent(gfx)
       Swing_Thread.assert()
+
       val buffer = model.buffer
       Isabelle.buffer_lock(buffer) {
         val snapshot = model.snapshot()
+
+        def line_range(command: Command, start: Text.Offset): Option[(Int, Int)] =
+        {
+          try {
+            val line1 = buffer.getLineOfOffset(snapshot.convert(start))
+            val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
+            Some((line1, line2))
+          }
+          catch { case e: ArrayIndexOutOfBoundsException => None }
+        }
         for {
           (command, start) <- snapshot.node.command_starts
           if !command.is_ignored
-          val line1 = buffer.getLineOfOffset(snapshot.convert(start))
-          val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
+          (line1, line2) <- line_range(command, start)
           val y = line_to_y(line1)
           val height = HEIGHT * (line2 - line1)
           color <- Isabelle_Markup.overview_color(snapshot, command)