# HG changeset patch # User wenzelm # Date 1308751290 -7200 # Node ID 0aca4edbfa99ee59ad7e7b11fd25dc3b340a253d # Parent 4ffb4ca04fb88b1e3cd5084baa9f276c6daa4c77 clarified chunk.offset, chunk.length; diff -r 4ffb4ca04fb8 -r 0aca4edbfa99 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