# HG changeset patch # User wenzelm # Date 1310415551 -7200 # Node ID d93a69672362a0a418c75870acbfec3761bc9761 # Parent 52310132063bc6c4cf48d592e7a43c3f14611c70 more uniform padded_markup, which is important for caret visibility despite absence of markup; diff -r 52310132063b -r d93a69672362 src/Tools/jEdit/src/text_area_painter.scala --- a/src/Tools/jEdit/src/text_area_painter.scala Mon Jul 11 17:22:31 2011 +0200 +++ b/src/Tools/jEdit/src/text_area_painter.scala Mon Jul 11 22:19:11 2011 +0200 @@ -214,37 +214,33 @@ r2 <- r1.try_restrict(chunk_range) } yield r2 + val padded_markup = + if (markup.isEmpty) + Iterator(Text.Info(chunk_range, None)) + else + Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++ + markup.iterator ++ + Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None)) + var x1 = x + w gfx.setFont(chunk_font) - if (markup.isEmpty) { - gfx.setColor(chunk_color) - gfx.drawString(chunk.str, x1, y) - } - else { - for { - Text.Info(range, info) <- - Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++ - markup.iterator ++ - Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None)) - if !range.is_singularity - } { - val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset) - gfx.setColor(info.getOrElse(chunk_color)) + for (Text.Info(range, info) <- padded_markup if !range.is_singularity) { + 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 { - case Some(r) if !r.is_singularity => - val astr = new AttributedString(str) - val i = r.start - range.start - val j = r.stop - range.start - astr.addAttribute(TextAttribute.FONT, chunk_font) - astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j) - astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j) - gfx.drawString(astr.getIterator, x1, y) - case _ => - gfx.drawString(str, x1, y) - } - x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat + range.try_restrict(caret_range) match { + case Some(r) if !r.is_singularity => + val astr = new AttributedString(str) + val i = r.start - range.start + val j = r.stop - range.start + astr.addAttribute(TextAttribute.FONT, chunk_font) + astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j) + astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j) + gfx.drawString(astr.getIterator, x1, y) + case _ => + gfx.drawString(str, x1, y) } + x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat } } w += chunk.width