--- a/src/Tools/jEdit/src/text_area_painter.scala Wed Jun 22 16:01:30 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala Wed Jun 22 16:32:36 2011 +0200
@@ -198,8 +198,7 @@
while (chunk != null) {
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)
+ x + w < clip_rect.x + clip_rect.width && chunk.accessable)
{
val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
val chunk_font = chunk.style.getFont