1.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 28 18:51:10 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 28 20:22:58 2010 +0200
     1.3 @@ -364,14 +364,24 @@
     1.4      {
     1.5        super.paintComponent(gfx)
     1.6        Swing_Thread.assert()
     1.7 +
     1.8        val buffer = model.buffer
     1.9        Isabelle.buffer_lock(buffer) {
    1.10          val snapshot = model.snapshot()
    1.11 +
    1.12 +        def line_range(command: Command, start: Text.Offset): Option[(Int, Int)] =
    1.13 +        {
    1.14 +          try {
    1.15 +            val line1 = buffer.getLineOfOffset(snapshot.convert(start))
    1.16 +            val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
    1.17 +            Some((line1, line2))
    1.18 +          }
    1.19 +          catch { case e: ArrayIndexOutOfBoundsException => None }
    1.20 +        }
    1.21          for {
    1.22            (command, start) <- snapshot.node.command_starts
    1.23            if !command.is_ignored
    1.24 -          val line1 = buffer.getLineOfOffset(snapshot.convert(start))
    1.25 -          val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
    1.26 +          (line1, line2) <- line_range(command, start)
    1.27            val y = line_to_y(line1)
    1.28            val height = HEIGHT * (line2 - line1)
    1.29            color <- Isabelle_Markup.overview_color(snapshot, command)