# HG changeset patch
# User wenzelm
# Date 1283285035 -7200
# Node ID 9210cf2b486909cbd42615a369074309fa62d1d7
# Parent  06582837872b03452e482334dc4860eea6723376
tuned;

diff -r 06582837872b -r 9210cf2b4869 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Aug 31 19:55:43 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Aug 31 22:03:55 2010 +0200
@@ -158,13 +158,12 @@
   {
     override def paintScreenLineRange(gfx: Graphics2D,
       first_line: Int, last_line: Int, physical_lines: Array[Int],
-      start: Array[Int], end: Array[Int], y0: Int, line_height: Int)
+      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       Isabelle.swing_buffer_lock(model.buffer) {
         val snapshot = model.snapshot()
         val saved_color = gfx.getColor
         try {
-          var y = y0
           for (i <- 0 until physical_lines.length) {
             if (physical_lines(i) != -1) {
               val line_range = proper_line_range(start(i), end(i))
@@ -175,11 +174,10 @@
                 val q = text_area.offsetToXY(range.stop)
                 if (p != null && q != null) {
                   gfx.setColor(Document_View.choose_color(snapshot, command))
-                  gfx.fillRect(p.x, y, q.x - p.x, line_height)
+                  gfx.fillRect(p.x, y + i * line_height, q.x - p.x, line_height)
                 }
               }
             }
-            y += line_height
           }
         }
         finally { gfx.setColor(saved_color) }