src/Tools/jEdit/src/text_area_painter.scala
changeset 43506 bf7400573617
parent 43505 0aca4edbfa99
child 43759 d93a69672362
     1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 22 16:01:30 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Wed Jun 22 16:32:36 2011 +0200
     1.3 @@ -198,8 +198,7 @@
     1.4      while (chunk != null) {
     1.5        val chunk_offset = line_start + chunk.offset
     1.6        if (x + w + chunk.width > clip_rect.x &&
     1.7 -          x + w < clip_rect.x + clip_rect.width &&
     1.8 -          chunk.accessable && chunk.visible)
     1.9 +          x + w < clip_rect.x + clip_rect.width && chunk.accessable)
    1.10        {
    1.11          val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
    1.12          val chunk_font = chunk.style.getFont