1.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Feb 20 15:36:48 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Feb 20 20:24:01 2012 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 +import scala.annotation.tailrec
     1.8  import scala.collection.mutable
     1.9  import scala.collection.immutable.SortedMap
    1.10  import scala.actors.Actor._
    1.11 @@ -354,11 +355,7 @@
    1.12      private val WIDTH = 10
    1.13      private val HEIGHT = 2
    1.14  
    1.15 -    private def line_to_y(line: Int): Int =
    1.16 -      (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
    1.17 -
    1.18 -    private def y_to_line(y: Int): Int =
    1.19 -      (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
    1.20 +    private def lines(): Int = model.buffer.getLineCount max text_area.getVisibleLines
    1.21  
    1.22      setPreferredSize(new Dimension(WIDTH, 0))
    1.23  
    1.24 @@ -366,7 +363,7 @@
    1.25  
    1.26      addMouseListener(new MouseAdapter {
    1.27        override def mousePressed(event: MouseEvent) {
    1.28 -        val line = y_to_line(event.getY)
    1.29 +        val line = (event.getY * lines()) / getHeight
    1.30          if (line >= 0 && line < text_area.getLineCount)
    1.31            text_area.setCaretPosition(text_area.getLineStartOffset(line))
    1.32        }
    1.33 @@ -391,20 +388,39 @@
    1.34        Isabelle.buffer_lock(buffer) {
    1.35          val snapshot = update_snapshot()
    1.36  
    1.37 -        for {
    1.38 -          line <- 0 until buffer.getLineCount
    1.39 -          range <-
    1.40 -            try {
    1.41 -              Some(proper_line_range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line)))
    1.42 +        gfx.setColor(getBackground)
    1.43 +        gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
    1.44 +
    1.45 +        val line_count = model.buffer.getLineCount
    1.46 +        val char_count = model.buffer.getLength
    1.47 +
    1.48 +        val L = lines()
    1.49 +        val H = getHeight()
    1.50 +
    1.51 +        @tailrec def paint_loop(l: Int, h: Int, p: Int, q: Int): Unit =
    1.52 +        {
    1.53 +          if (l < line_count && h < H) {
    1.54 +            val p1 = p + H
    1.55 +            val q1 = q + L
    1.56 +            val (l1, h1) =
    1.57 +              if (p1 >= q1) (l + 1, h + (p1 - q) / L)
    1.58 +              else (l + (q1 - p) / H, h + 1)
    1.59 +
    1.60 +            val start = model.buffer.getLineStartOffset(l)
    1.61 +            val end =
    1.62 +              if (l1 < line_count) model.buffer.getLineStartOffset(l1)
    1.63 +              else char_count
    1.64 +
    1.65 +            Isabelle_Rendering.overview_color(snapshot, Text.Range(start, end)) match {
    1.66 +              case None =>
    1.67 +              case Some(color) =>
    1.68 +                gfx.setColor(color)
    1.69 +                gfx.fillRect(0, h, getWidth, h1 - h)
    1.70              }
    1.71 -            catch { case e: ArrayIndexOutOfBoundsException => None }
    1.72 -          color <- Isabelle_Rendering.overview_color(snapshot, range)
    1.73 -        } {
    1.74 -          val y = line_to_y(line)
    1.75 -          val h = (line_to_y(line + 1) - y) max 2
    1.76 -          gfx.setColor(color)
    1.77 -          gfx.fillRect(0, y, getWidth - 1, h)
    1.78 +            paint_loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L)
    1.79 +          }
    1.80          }
    1.81 +        paint_loop(0, 0, 0, 0)
    1.82        }
    1.83      }
    1.84    }