# HG changeset patch
# User wenzelm
# Date 1460723279 -7200
# Node ID 35f1475e9ced0f41c5893183dba67f55e2582ddf
# Parent  7b0f0398d33f3306f233442bf528fc204b0c4f4f
clarified rendering wrt. hyperlinks;

diff -r 7b0f0398d33f -r 35f1475e9ced src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Fri Apr 15 13:02:23 2016 +0200
+++ b/src/Tools/jEdit/etc/options	Fri Apr 15 14:27:59 2016 +0200
@@ -100,7 +100,7 @@
 option bad_color : string = "FF6A6A64"
 option intensify_color : string = "FFCC6664"
 option entity_color : string = "CCD9FF80"
-option entity_def_color : string = "800080FF"
+option entity_ref_color : string = "800080FF"
 option breakpoint_disabled_color : string = "CCCC0080"
 option breakpoint_enabled_color : string = "FF9966FF"
 option quoted_color : string = "8B8B8B19"
diff -r 7b0f0398d33f -r 35f1475e9ced src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Fri Apr 15 13:02:23 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Apr 15 14:27:59 2016 +0200
@@ -254,7 +254,7 @@
   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")
@@ -428,11 +428,11 @@
     else Set.empty[Long]
   }
 
-  def entity_def(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] =
+  def entity_ref(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 Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _)) if focus(i) =>
+          Some(entity_ref_color)
         case _ => None
       })
 
diff -r 7b0f0398d33f -r 35f1475e9ced src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Apr 15 13:02:23 2016 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Apr 15 14:27:59 2016 +0200
@@ -571,7 +571,7 @@
             // entity def range
             if (!area_active() && caret_visible) {
               for {
-                Text.Info(range, color) <- rendering.entity_def(line_range, caret_focus)
+                Text.Info(range, color) <- rendering.entity_ref(line_range, caret_focus)
                 r <- JEdit_Lib.gfx_range(text_area, range)
               } {
                 gfx.setColor(color)