# HG changeset patch # User wenzelm # Date 1465221145 -7200 # Node ID bf98cc9e6e0647ec4474ddfc91c4eef7bb23e88d # Parent 2eb2ff479cfe788601fe20b550b49adad9692e43 tuned; diff -r 2eb2ff479cfe -r bf98cc9e6e06 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Mon Jun 06 14:16:25 2016 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Mon Jun 06 15:52:25 2016 +0200 @@ -418,20 +418,20 @@ } val focus_defs = focus(true) + if (focus_defs.nonEmpty) focus_defs else { val focus_refs = focus(false) - - def active(range: Text.Range): Boolean = - snapshot.cumulate[Boolean](range, false, Rendering.caret_focus_elements, _ => + def visible_def: Boolean = + 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_refs(i) => Some(true) case _ => None } - }).exists({ case Text.Info(_, visible) => visible }) - if (focus_refs.nonEmpty && (active(caret_range) || active(visible_range))) focus_refs + }).exists(info => info.info) + if (focus_refs.nonEmpty && visible_def) focus_refs else Set.empty[Long] } }