tuned rendering;

--- a/src/Tools/jEdit/etc/options	Thu Apr 14 23:31:10 2016 +0200
+++ b/src/Tools/jEdit/etc/options	Fri Apr 15 12:07:53 2016 +0200
@@ -99,8 +99,8 @@
 option spell_checker_color : string = "0000FFFF"
 option bad_color : string = "FF6A6A64"
 option intensify_color : string = "FFCC6664"
-option entity_def_color : string = "CCD9FFA0"
-option entity_ref_color : string = "E6FFCCA0"
+option entity_color : string = "CCD9FF80"
+option entity_def_color : string = "800080FF"
 option breakpoint_disabled_color : string = "CCCC0080"
 option breakpoint_enabled_color : string = "FF9966FF"
 option quoted_color : string = "8B8B8B19"

--- a/src/Tools/jEdit/src/rendering.scala	Thu Apr 14 23:31:10 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Apr 15 12:07:53 2016 +0200
@@ -253,8 +253,8 @@
   val spell_checker_color = color_value("spell_checker_color")
   val bad_color = color_value("bad_color")
   val intensify_color = color_value("intensify_color")
+  val entity_color = color_value("entity_color")
   val entity_def_color = color_value("entity_def_color")
-  val entity_ref_color = color_value("entity_ref_color")
   val breakpoint_disabled_color = color_value("breakpoint_disabled_color")
   val breakpoint_enabled_color = color_value("breakpoint_enabled_color")
   val caret_debugger_color = color_value("caret_debugger_color")
@@ -427,6 +427,14 @@
     if (visible) focus else Set.empty[Long]
   }
 
+  def entity_def(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] =
+    snapshot.select(range, Rendering.caret_focus_elements, _ =>
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Def(i)), _)) if focus(i) =>
+          Some(entity_def_color)
+        case _ => None
+      })
+
 
   /* highlighted area */
 
@@ -750,10 +758,8 @@
                 Some((Nil, Some(intensify_color)))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
                 props match {
-                  case Markup.Entity.Def(i) if focus(i) =>
-                    Some((Nil, Some(entity_def_color)))
-                  case Markup.Entity.Ref(i) if focus(i) =>
-                    Some((Nil, Some(entity_ref_color)))
+                  case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(entity_color)))
+                  case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(entity_color)))
                   case _ => None
                 }
               case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) =>

--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Apr 14 23:31:10 2016 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Apr 15 12:07:53 2016 +0200
@@ -73,6 +73,7 @@
 
   @volatile private var painter_rendering: Rendering = null
   @volatile private var painter_clip: Shape = null
+  @volatile private var caret_focus: Set[Long] = Set.empty
 
   private val set_state = new TextAreaExtension
   {
@@ -82,6 +83,12 @@
     {
       painter_rendering = get_rendering()
       painter_clip = gfx.getClip
+      caret_focus =
+        JEdit_Lib.visible_range(text_area) match {
+          case Some(visible_range) if caret_enabled =>
+            painter_rendering.caret_focus(JEdit_Lib.caret_range(text_area), visible_range)
+          case _ => Set.empty[Long]
+        }
     }
   }
 
@@ -93,6 +100,7 @@
     {
       painter_rendering = null
       painter_clip = null
+      caret_focus = Set.empty
     }
   }
 
@@ -161,6 +169,9 @@
     List((highlight_area, true), (hyperlink_area, true), (active_area, false))
   def active_reset(): Unit = active_areas.foreach(_._1.reset)
 
+  private def area_active(): Boolean =
+    active_areas.exists({ case (area, _) => area.is_active })
+
   private val focus_listener = new FocusAdapter {
     override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } }
   }
@@ -280,13 +291,6 @@
       robust_rendering { rendering =>
         val fm = text_area.getPainter.getFontMetrics
 
-        val focus =
-          JEdit_Lib.visible_range(text_area) match {
-            case Some(visible_range) if caret_enabled =>
-              rendering.caret_focus(JEdit_Lib.caret_range(text_area), visible_range)
-            case _ => Set.empty[Long]
-          }
-
         for (i <- 0 until physical_lines.length) {
           if (physical_lines(i) != -1) {
             val line_range = Text.Range(start(i), end(i) min buffer.getLength)
@@ -301,7 +305,7 @@
 
             // background color
             for {
-              Text.Info(range, color) <- rendering.background(line_range, focus)
+              Text.Info(range, color) <- rendering.background(line_range, caret_focus)
               r <- JEdit_Lib.gfx_range(text_area, range)
             } {
               gfx.setColor(color)
@@ -564,8 +568,19 @@
               gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
             }
 
+            // entity def range
+            if (!area_active() && caret_visible) {
+              for {
+                Text.Info(range, color) <- rendering.entity_def(line_range, caret_focus)
+                r <- JEdit_Lib.gfx_range(text_area, range)
+              } {
+                gfx.setColor(color)
+                gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
+              }
+            }
+
             // completion range
-            if (!hyperlink_area.is_active && caret_visible) {
+            if (!area_active() && caret_visible) {
               for {
                 completion <- Completion_Popup.Text_Area(text_area)
                 Text.Info(range, color) <- completion.rendering(rendering, line_range)