--- a/src/Pure/PIDE/markup.scala Thu Apr 14 20:47:44 2016 +0200
+++ b/src/Pure/PIDE/markup.scala Thu Apr 14 22:55:53 2016 +0200
@@ -86,11 +86,12 @@
val BINDING = "binding"
val ENTITY = "entity"
- val DEF = "def"
- val REF = "ref"
object Entity
{
+ val Def = new Properties.Long("def")
+ val Ref = new Properties.Long("ref")
+
def unapply(markup: Markup): Option[(String, String)] =
markup match {
case Markup(ENTITY, props) =>
--- a/src/Tools/jEdit/etc/options Thu Apr 14 20:47:44 2016 +0200
+++ b/src/Tools/jEdit/etc/options Thu Apr 14 22:55:53 2016 +0200
@@ -99,6 +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 breakpoint_disabled_color : string = "CCCC0080"
option breakpoint_enabled_color : string = "FF9966FF"
option quoted_color : string = "8B8B8B19"
--- a/src/Tools/jEdit/src/document_view.scala Thu Apr 14 20:47:44 2016 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Thu Apr 14 22:55:53 2016 +0200
@@ -185,6 +185,7 @@
private val delay_caret_update =
GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
session.caret_focus.post(Session.Caret_Focus)
+ JEdit_Lib.invalidate(text_area)
}
private val caret_listener = new CaretListener {
@@ -219,26 +220,7 @@
changed.commands.exists(snapshot.node.commands.contains)))
text_overview.invoke()
- val visible_lines = text_area.getVisibleLines
- if (visible_lines > 0) {
- if (changed.assignment || load_changed)
- text_area.invalidateScreenLineRange(0, visible_lines)
- else {
- val visible_range = JEdit_Lib.visible_range(text_area).get
- val visible_iterator =
- snapshot.node.command_iterator(snapshot.revert(visible_range)).map(_._1)
- if (visible_iterator.exists(changed.commands)) {
- for {
- line <- (0 until visible_lines).iterator
- start = text_area.getScreenLineStartOffset(line) if start >= 0
- end = text_area.getScreenLineEndOffset(line) if end >= 0
- range = Text.Range(start, end)
- line_cmds = snapshot.node.command_iterator(snapshot.revert(range)).map(_._1)
- if line_cmds.exists(changed.commands)
- } text_area.invalidateScreenLineRange(line, line)
- }
- }
- }
+ JEdit_Lib.invalidate(text_area)
}
}
}
--- a/src/Tools/jEdit/src/jedit_lib.scala Thu Apr 14 20:47:44 2016 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Thu Apr 14 22:55:53 2016 +0200
@@ -234,6 +234,12 @@
}
}
+ def invalidate(text_area: TextArea)
+ {
+ val visible_lines = text_area.getVisibleLines
+ if (visible_lines > 0) text_area.invalidateScreenLineRange(0, visible_lines)
+ }
+
/* graphics range */
--- a/src/Tools/jEdit/src/rendering.scala Thu Apr 14 20:47:44 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Thu Apr 14 22:55:53 2016 +0200
@@ -151,6 +151,8 @@
private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT)
+ private val caret_focus_elements = Markup.Elements(Markup.ENTITY)
+
private val highlight_elements =
Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING,
@@ -206,7 +208,8 @@
Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
- Markup.BAD + Markup.INTENSIFY + Markup.Markdown_Item.name ++ active_elements
+ Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
+ Markup.Markdown_Item.name ++ active_elements
private val foreground_elements =
Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
@@ -250,6 +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_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")
@@ -392,6 +397,37 @@
}
+ /* caret focus */
+
+ def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
+ {
+ val focus_results =
+ snapshot.cumulate[Set[Long]](caret_range, Set.empty, Rendering.caret_focus_elements, _ =>
+ {
+ case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
+ props match {
+ case Markup.Entity.Def(i) => Some(serials + i)
+ case Markup.Entity.Ref(i) => Some(serials + i)
+ case _ => None
+ }
+ case _ => None
+ })
+ val focus = (Set.empty[Long] /: focus_results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
+
+ val visible =
+ focus.nonEmpty &&
+ snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ =>
+ {
+ case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
+ props match {
+ case Markup.Entity.Def(i) if focus(i) => Some(true)
+ case _ => None
+ }
+ }).exists({ case Text.Info(_, visible) => visible })
+ if (visible) focus else Set.empty[Long]
+ }
+
+
/* highlighted area */
def highlight(range: Text.Range): Option[Text.Info[Color]] =
@@ -697,7 +733,7 @@
/* text background */
- def background(range: Text.Range): List[Text.Info[Color]] =
+ def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] =
{
for {
Text.Info(r, result) <-
@@ -712,6 +748,14 @@
Some((Nil, Some(bad_color)))
case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
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 _ => None
+ }
case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) =>
val color =
depth match {
--- a/src/Tools/jEdit/src/rich_text_area.scala Thu Apr 14 20:47:44 2016 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Thu Apr 14 22:55:53 2016 +0200
@@ -280,6 +280,13 @@
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)
@@ -294,7 +301,7 @@
// background color
for {
- Text.Info(range, color) <- rendering.background(line_range)
+ Text.Info(range, color) <- rendering.background(line_range, focus)
r <- JEdit_Lib.gfx_range(text_area, range)
} {
gfx.setColor(color)