src/Pure/PIDE/rendering.scala

--- a/src/Pure/PIDE/rendering.scala	Mon Dec 14 16:51:12 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Mon Dec 14 22:01:54 2020 +0100
@@ -178,6 +178,13 @@
     val empty: Focus = apply(Set.empty)
     def make(args: List[Text.Info[Focus]]): Focus =
       (empty /: args)({ case (focus1, Text.Info(_, focus2)) => focus1 ++ focus2 })
+
+    val full: Focus =
+      new Focus(Set.empty)
+      {
+        override def apply(id: Long): Boolean = true
+        override def toString: String = "Focus.full"
+      }
   }
 
   sealed class Focus private[Rendering](protected val rep: Set[Long])
@@ -504,30 +511,36 @@
           case _ => None
         }))
 
-  def entity_focus(range: Text.Range, visible_defs: Rendering.Focus): Rendering.Focus =
+  def entity_focus(range: Text.Range, defs_focus: Rendering.Focus): Rendering.Focus =
     Rendering.Focus.make(
       snapshot.cumulate(range, Rendering.Focus.empty, Rendering.entity_elements, _ =>
         {
           case (focus, Text.Info(_, XML.Elem(Markup.Entity.Ref(i), _)))
-          if visible_defs(i) => Some(focus + i)
+          if defs_focus(i) => Some(focus + i)
           case _ => None
         }))
 
 
   /* caret focus */
 
-  def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Rendering.Focus =
+  def caret_focus(caret_range: Text.Range, defs_range: Text.Range): Rendering.Focus =
   {
     val focus = entity_focus_defs(caret_range)
     if (focus.defined) focus
-    else entity_focus(caret_range, entity_focus_defs(visible_range))
+    else if (defs_range == Text.Range.offside) Rendering.Focus.empty
+    else {
+      val defs_focus =
+        if (defs_range == Text.Range.full) Rendering.Focus.full
+        else entity_focus_defs(defs_range)
+      entity_focus(caret_range, defs_focus)
+    }
   }
 
-  def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
+  def caret_focus_ranges(caret_range: Text.Range, defs_range: Text.Range): List[Text.Range] =
   {
-    val focus = caret_focus(caret_range, visible_range)
+    val focus = caret_focus(caret_range, defs_range)
     if (focus.defined) {
-      snapshot.cumulate[Boolean](visible_range, false, Rendering.entity_elements, _ =>
+      snapshot.cumulate[Boolean](defs_range, false, Rendering.entity_elements, _ =>
         {
           case (_, Text.Info(_, XML.Elem(Markup.Entity.Id(i), _))) if focus(i) => Some(true)
           case _ => None