tuned signature;

--- a/src/Pure/PIDE/rendering.scala	Sun Dec 13 16:35:37 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sun Dec 13 17:48:51 2020 +0100
@@ -176,6 +176,7 @@
   {
     def apply(ids: Set[Long]): Focus = new Focus(ids)
     val empty: Focus = apply(Set.empty)
+    def merge(args: TraversableOnce[Focus]): Focus = (empty /: args)(_ ++ _)
   }
 
   sealed class Focus private[Rendering](protected val rep: Set[Long])
@@ -239,7 +240,7 @@
   val warning_elements = Markup.Elements(Markup.WARNING, Markup.LEGACY)
   val error_elements = Markup.Elements(Markup.ERROR)
 
-  val entity_focus_elements = Markup.Elements(Markup.ENTITY)
+  val entity_elements = Markup.Elements(Markup.ENTITY)
 
   val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED)
 
@@ -502,9 +503,9 @@
       check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def)
     : Rendering.Focus =
   {
-    val results =
-      snapshot.cumulate[Rendering.Focus](range, Rendering.Focus.empty,
-        Rendering.entity_focus_elements, _ =>
+    Rendering.Focus.merge(
+      snapshot.cumulate[Rendering.Focus](range, Rendering.Focus.empty, Rendering.entity_elements,
+        _ =>
           {
             case (focus, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
               props match {
@@ -513,9 +514,7 @@
                 case _ => None
               }
             case _ => None
-          })
-    (Rendering.Focus.empty /: results){
-      case (focus1, Text.Info(_, focus2)) => focus1 ++ focus2 }
+          }).iterator.map(_.info))
   }
 
   def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Rendering.Focus =
@@ -533,7 +532,7 @@
     val focus = caret_focus(caret_range, visible_range)
     if (focus.defined) {
       val results =
-        snapshot.cumulate[Boolean](visible_range, false, Rendering.entity_focus_elements, _ =>
+        snapshot.cumulate[Boolean](visible_range, false, Rendering.entity_elements, _ =>
           {
             case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
               props match {

--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sun Dec 13 16:35:37 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sun Dec 13 17:48:51 2020 +0100
@@ -225,7 +225,7 @@
   /* caret focus */
 
   def entity_ref(range: Text.Range, focus: Rendering.Focus): List[Text.Info[Color]] =
-    snapshot.select(range, Rendering.entity_focus_elements, _ =>
+    snapshot.select(range, Rendering.entity_elements, _ =>
       {
         case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _))
         if focus(i) => Some(entity_ref_color)