# 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]
     }
   }