--- 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)