# HG changeset patch
# User wenzelm
# Date 1393413349 -3600
# Node ID 6a16443e520e880139c34e9824c581023002dc30
# Parent  ec7ca5388dead9ebbbab9dae66e76203978c2fe2
improved rendering of blinking cursor;

diff -r ec7ca5388dea -r 6a16443e520e src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Feb 26 11:58:35 2014 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Feb 26 12:15:49 2014 +0100
@@ -295,6 +295,9 @@
 
   /* text */
 
+  private def caret_enabled: Boolean =
+    caret_visible && (!text_area.hasFocus || text_area.isCaretVisible)
+
   private def caret_color(rendering: Rendering): Color =
   {
     if (text_area.isCaretVisible)
@@ -310,7 +313,7 @@
     val font_context = painter.getFontRenderContext
 
     val caret_range =
-      if (caret_visible) JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
+      if (caret_enabled) JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
       else Text.Range(-1)
 
     var w = 0.0f
@@ -526,7 +529,7 @@
       robust_rendering { rendering =>
         if (caret_visible) {
           val caret = text_area.getCaretPosition
-          if (start <= caret && caret == end - 1) {
+          if (caret_enabled && start <= caret && caret == end - 1) {
             val painter = text_area.getPainter
             val fm = painter.getFontMetrics
             val metric = JEdit_Lib.pretty_metric(painter)