tuned;

--- a/src/Pure/PIDE/rendering.scala	Mon Dec 14 16:40:33 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Mon Dec 14 16:51:12 2020 +0100
@@ -525,12 +525,11 @@
 
   def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
   {
-    val focus_defs = caret_focus(caret_range, visible_range)
-    if (focus_defs.defined) {
+    val focus = caret_focus(caret_range, visible_range)
+    if (focus.defined) {
       snapshot.cumulate[Boolean](visible_range, false, Rendering.entity_elements, _ =>
         {
-          case (_, Text.Info(_, XML.Elem(Markup.Entity.Id(i), _)))
-          if focus_defs(i) => Some(true)
+          case (_, Text.Info(_, XML.Elem(Markup.Entity.Id(i), _))) if focus(i) => Some(true)
           case _ => None
         }).flatMap(info => if (info.info) Some(info.range) else None)
     }