--- a/src/Tools/jEdit/src/text_area_painter.scala Sat Apr 14 18:28:11 2012 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala Sat Apr 14 19:09:34 2012 +0200
@@ -220,7 +220,7 @@
else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
val caret_range =
- if (text_area.hasFocus) doc_view.caret_range()
+ if (text_area.isCaretVisible) doc_view.caret_range()
else Text.Range(-1)
val markup =
@@ -373,7 +373,7 @@
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
{
robust_snapshot { _ =>
- if (text_area.hasFocus) {
+ if (text_area.isCaretVisible) {
val caret = text_area.getCaretPosition
if (start <= caret && caret == end - 1) {
val painter = text_area.getPainter