clarified chunk.offset, chunk.length;
authorwenzelm
Wed, 22 Jun 2011 16:01:30 +0200
changeset 43505 0aca4edbfa99
parent 43504 4ffb4ca04fb8
child 43506 bf7400573617
clarified chunk.offset, chunk.length;
src/Tools/jEdit/src/text_area_painter.scala
--- a/src/Tools/jEdit/src/text_area_painter.scala	Tue Jun 21 23:08:16 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 22 16:01:30 2011 +0200
@@ -187,23 +187,21 @@
   }
 
   private def paint_chunk_list(
-    gfx: Graphics2D, offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
+    gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   {
     val clip_rect = gfx.getClipBounds
     val painter = text_area.getPainter
     val font_context = painter.getFontRenderContext
 
     var w = 0.0f
-    var chunk_offset = offset
     var chunk = head
     while (chunk != null) {
-      val chunk_length = if (chunk.str == null) 0 else chunk.str.length
-
+      val chunk_offset = line_start + chunk.offset
       if (x + w + chunk.width > clip_rect.x &&
           x + w < clip_rect.x + clip_rect.width &&
           chunk.accessable && chunk.visible)
       {
-        val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk_length)
+        val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
         val chunk_font = chunk.style.getFont
         val chunk_color = chunk.style.getForegroundColor
 
@@ -251,7 +249,6 @@
         }
       }
       w += chunk.width
-      chunk_offset += chunk_length
       chunk = chunk.next.asInstanceOf[Chunk]
     }
     w