# HG changeset patch
# User wenzelm
# Date 1393266819 -3600
# Node ID 945ad7eaf37f82e32ea876ef15ffc3f31d4a6044
# Parent  9d605a21d7ec0b9572caa41e357ea015d17b2fa6
tuned colors;

diff -r 9d605a21d7ec -r 945ad7eaf37f src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Mon Feb 24 14:58:40 2014 +0100
+++ b/src/Tools/jEdit/etc/options	Mon Feb 24 19:33:39 2014 +0100
@@ -85,7 +85,7 @@
 option keyword1_color : string = "006699FF"
 option keyword2_color : string = "009966FF"
 option keyword3_color : string = "0099FFFF"
-option caret_invisible_color : string = "99999980"
+option caret_invisible_color : string = "50000080"
 
 option tfree_color : string = "A020F0FF"
 option tvar_color : string = "A020F0FF"
diff -r 9d605a21d7ec -r 945ad7eaf37f src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Feb 24 14:58:40 2014 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Feb 24 19:33:39 2014 +0100
@@ -456,6 +456,7 @@
     {
       robust_rendering { rendering =>
         val caret_range = get_caret_range(true)
+        val caret_color = text_area.getPainter.getCaretColor
 
         for (i <- 0 until physical_lines.length) {
           if (physical_lines(i) != -1) {
@@ -494,7 +495,7 @@
             if (!hyperlink_area.is_active) {
               def paint_completion(range: Text.Range) {
                 for (r <- JEdit_Lib.gfx_range(text_area, range)) {
-                  gfx.setColor(get_caret_color(rendering))
+                  gfx.setColor(caret_color)
                   gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
                 }
               }