1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Fri Sep 02 21:48:27 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Fri Sep 02 22:48:56 2011 +0200
     1.3 @@ -201,6 +201,7 @@
     1.4            x + w < clip_rect.x + clip_rect.width && chunk.accessable)
     1.5        {
     1.6          val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
     1.7 +        val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
     1.8          val chunk_font = chunk.style.getFont
     1.9          val chunk_color = chunk.style.getForegroundColor
    1.10  
    1.11 @@ -229,7 +230,7 @@
    1.12          var x1 = x + w
    1.13          gfx.setFont(chunk_font)
    1.14          for (Text.Info(range, info) <- padded_markup if !range.is_singularity) {
    1.15 -          val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
    1.16 +          val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
    1.17            gfx.setColor(info.getOrElse(chunk_color))
    1.18  
    1.19            range.try_restrict(caret_range) match {