# HG changeset patch
# User wenzelm
# Date 1314996536 -7200
# Node ID c8f1d943bfc5fbddb0bcb45a6a4df961d123bcd8
# Parent  383c9d758a56247577ca129169bb7ad9bcc4ffd0
more robust chunk painting wrt. hard tabs, when chunk.str == null;

diff -r 383c9d758a56 -r c8f1d943bfc5 src/Tools/jEdit/src/text_area_painter.scala
--- 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 {