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