# HG changeset patch
# User wenzelm
# Date 1460718105 -7200
# Node ID ed8739792e8a17a46586ff5671732fb2eb93b82b
# Parent  224e8d8a4fb8adc7e6b7397975531666ac803497
clarified focus visibility;

diff -r 224e8d8a4fb8 -r ed8739792e8a src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Fri Apr 15 12:07:53 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Apr 15 13:01:45 2016 +0200
@@ -414,17 +414,18 @@
           })
     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]
+    def visible_focus(range: Text.Range): Boolean =
+      snapshot.cumulate[Boolean](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 (focus.nonEmpty && (visible_focus(caret_range) || visible_focus(visible_range))) focus
+    else Set.empty[Long]
   }
 
   def entity_def(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] =