# HG changeset patch
# User wenzelm
# Date 1393242715 -3600
# Node ID 734ac5709fbe70f0e0ec78fc55df1c121c4776dc
# Parent  e757e8c8d8ea4878d44dedfc7a265cbdf4adb583
clarified painting of invisible caret, e.g. focus change due to popup;

diff -r e757e8c8d8ea -r 734ac5709fbe src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Mon Feb 24 12:23:35 2014 +0100
+++ b/src/Tools/jEdit/etc/options	Mon Feb 24 12:51:55 2014 +0100
@@ -85,6 +85,7 @@
 option keyword1_color : string = "006699FF"
 option keyword2_color : string = "009966FF"
 option keyword3_color : string = "0099FFFF"
+option caret_invisible_color : string = "99999980"
 
 option tfree_color : string = "A020F0FF"
 option tvar_color : string = "A020F0FF"
diff -r e757e8c8d8ea -r 734ac5709fbe src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Feb 24 12:23:35 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Feb 24 12:51:55 2014 +0100
@@ -260,6 +260,7 @@
   val keyword1_color = color_value("keyword1_color")
   val keyword2_color = color_value("keyword2_color")
   val keyword3_color = color_value("keyword3_color")
+  val caret_invisible_color = color_value("caret_invisible_color")
 
   val tfree_color = color_value("tfree_color")
   val tvar_color = color_value("tvar_color")
diff -r e757e8c8d8ea -r 734ac5709fbe src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Feb 24 12:23:35 2014 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Feb 24 12:51:55 2014 +0100
@@ -222,16 +222,25 @@
   }
 
 
-  /* text background */
+  /* caret */
 
   private def get_caret_range(stretch: Boolean): Text.Range =
-    if (caret_visible && text_area.isCaretVisible) {
+    if (caret_visible) {
       val caret = text_area.getCaretPosition
       if (stretch) JEdit_Lib.stretch_point_range(buffer, caret)
       else JEdit_Lib.point_range(buffer, caret)
     }
     else Text.Range(-1)
 
+  private def get_caret_color(rendering: Rendering): Color =
+  {
+    if (text_area.isCaretVisible) text_area.getPainter.getCaretColor
+    else rendering.caret_invisible_color
+  }
+
+
+  /* text background */
+
   private val background_painter = new TextAreaExtension
   {
     override def paintScreenLineRange(gfx: Graphics2D,
@@ -360,7 +369,7 @@
 
               val astr = new AttributedString(s2)
               astr.addAttribute(TextAttribute.FONT, chunk_font)
-              astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor)
+              astr.addAttribute(TextAttribute.FOREGROUND, get_caret_color(rendering))
               astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
               gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
 
@@ -446,7 +455,6 @@
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       robust_rendering { rendering =>
-        val painter = text_area.getPainter
         val caret_range = get_caret_range(true)
 
         for (i <- 0 until physical_lines.length) {
@@ -486,7 +494,7 @@
             if (!hyperlink_area.is_active) {
               def paint_completion(range: Text.Range) {
                 for (r <- JEdit_Lib.gfx_range(text_area, range)) {
-                  gfx.setColor(painter.getCaretColor)
+                  gfx.setColor(get_caret_color(rendering))
                   gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
                 }
               }
@@ -531,8 +539,8 @@
     override def paintValidLine(gfx: Graphics2D,
       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
     {
-      robust_rendering { _ =>
-        if (caret_visible && text_area.isCaretVisible) {
+      robust_rendering { rendering =>
+        if (caret_visible) {
           val caret = text_area.getCaretPosition
           if (start <= caret && caret == end - 1) {
             val painter = text_area.getPainter
@@ -541,7 +549,7 @@
 
             val offset = caret - text_area.getLineStartOffset(physical_line)
             val x = text_area.offsetToXY(physical_line, offset).x
-            gfx.setColor(painter.getCaretColor)
+            gfx.setColor(get_caret_color(rendering))
             gfx.drawRect(x, y, (metric.unit * metric.average).round.toInt - 1, fm.getHeight - 1)
           }
         }