src/Tools/jEdit/src/text_area_painter.scala
changeset 43505 0aca4edbfa99
parent 43451 be760a642d38
child 43506 bf7400573617
     1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Tue Jun 21 23:08:16 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 22 16:01:30 2011 +0200
     1.3 @@ -187,23 +187,21 @@
     1.4    }
     1.5  
     1.6    private def paint_chunk_list(
     1.7 -    gfx: Graphics2D, offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
     1.8 +    gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
     1.9    {
    1.10      val clip_rect = gfx.getClipBounds
    1.11      val painter = text_area.getPainter
    1.12      val font_context = painter.getFontRenderContext
    1.13  
    1.14      var w = 0.0f
    1.15 -    var chunk_offset = offset
    1.16      var chunk = head
    1.17      while (chunk != null) {
    1.18 -      val chunk_length = if (chunk.str == null) 0 else chunk.str.length
    1.19 -
    1.20 +      val chunk_offset = line_start + chunk.offset
    1.21        if (x + w + chunk.width > clip_rect.x &&
    1.22            x + w < clip_rect.x + clip_rect.width &&
    1.23            chunk.accessable && chunk.visible)
    1.24        {
    1.25 -        val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk_length)
    1.26 +        val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
    1.27          val chunk_font = chunk.style.getFont
    1.28          val chunk_color = chunk.style.getForegroundColor
    1.29  
    1.30 @@ -251,7 +249,6 @@
    1.31          }
    1.32        }
    1.33        w += chunk.width
    1.34 -      chunk_offset += chunk_length
    1.35        chunk = chunk.next.asInstanceOf[Chunk]
    1.36      }
    1.37      w