clarified rendering wrt. hyperlinks;
--- 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"
--- 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
})
--- 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)