# HG changeset patch
# User wenzelm
# Date 1607961072 -3600
# Node ID 71618a89a4e9a25546681aa9541ab5cdaef03a62
# Parent  cd6f6e2fe99dc6a7596cdf3145c96f4dd0b5a45e
tuned;

diff -r cd6f6e2fe99d -r 71618a89a4e9 src/Pure/PIDE/rendering.scala
--- 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)
     }