# HG changeset patch
# User wenzelm
# Date 1307967753 -7200
# Node ID 09d992ab57c65b944a64b8b3f0163c85e54b9a47
# Parent  df1be524e60c43841e85e1ae97b7e2a21fdc6944
imitate original Chunk.paintChunkList;

diff -r df1be524e60c -r 09d992ab57c6 src/Tools/jEdit/src/text_painter.scala
--- a/src/Tools/jEdit/src/text_painter.scala	Mon Jun 13 13:53:41 2011 +0200
+++ b/src/Tools/jEdit/src/text_painter.scala	Mon Jun 13 14:22:33 2011 +0200
@@ -31,8 +31,31 @@
 
   override def paintScreenLineRange(gfx: Graphics2D,
     first_line: Int, last_line: Int, physical_lines: Array[Int],
-    start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+    start: Array[Int], end: Array[Int], y_start: Int, line_height: Int)
   {
+    def paint_chunk_list(head: Chunk, x: Float, y: Float): Float =
+    {
+      val clip_rect = gfx.getClipBounds
+      var w = 0.0f
+      var chunk = head
+      while (chunk != null) {
+        if (x + w + chunk.width > clip_rect.x &&
+            x + w < clip_rect.x + clip_rect.width &&
+            chunk.accessable && chunk.visible)
+        {
+          gfx.setFont(chunk.style.getFont)
+          gfx.setColor(chunk.style.getForegroundColor)
+          if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null)
+            gfx.drawGlyphVector(chunk.gv, x + w, y)
+          else if (chunk.str != null)
+            gfx.drawString(chunk.str, (x + w).toInt, y.toInt)
+        }
+        w += chunk.width
+        chunk = chunk.next.asInstanceOf[Chunk]
+      }
+      w
+    }
+
     val buffer = text_area.getBuffer
     Isabelle.swing_buffer_lock(buffer) {
       val painter = text_area.getPainter
@@ -75,15 +98,15 @@
 
       val clip = gfx.getClip
       val x0 = text_area.getHorizontalOffset
-      var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
+      var y0 = y_start + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
       for (i <- 0 until physical_lines.length) {
         if (physical_lines(i) != -1) {
           line_infos.get(start(i)) match {
             case Some(chunk) =>
-              val w = Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR).toInt
+              val w = paint_chunk_list(chunk, x0, y0).toInt
               gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
-              orig_text_painter.paintValidLine(
-                gfx, first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
+              orig_text_painter.paintValidLine(gfx,
+                first_line + i, physical_lines(i), start(i), end(i), y_start + line_height * i)
               gfx.setClip(clip)
 
             case None =>