# HG changeset patch
# User wenzelm
# Date 1607896467 -3600
# Node ID 82570cae3cc2120b1bfc32875bb207b612ab02b5
# Parent  b44b2d2380f0798d6c76a2c231f64f8e9589b5c2
tuned;

diff -r b44b2d2380f0 -r 82570cae3cc2 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sun Dec 13 22:43:51 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sun Dec 13 22:54:27 2020 +0100
@@ -176,7 +176,8 @@
   {
     def apply(ids: Set[Long]): Focus = new Focus(ids)
     val empty: Focus = apply(Set.empty)
-    def merge(args: TraversableOnce[Focus]): Focus = (empty /: args)(_ ++ _)
+    def make(args: List[Text.Info[Focus]]): Focus =
+      (empty /: args)({ case (focus1, Text.Info(_, focus2)) => focus1 ++ focus2 })
   }
 
   sealed class Focus private[Rendering](protected val rep: Set[Long])
@@ -496,21 +497,21 @@
   /* entity focus */
 
   def entity_focus_defs(range: Text.Range): Rendering.Focus =
-    Rendering.Focus.merge(
-      snapshot.cumulate[Rendering.Focus](range, Rendering.Focus.empty, Rendering.entity_elements, _ =>
+    Rendering.Focus.make(
+      snapshot.cumulate(range, Rendering.Focus.empty, Rendering.entity_elements, _ =>
         {
           case (focus, Text.Info(_, XML.Elem(Markup.Entity.Def(i), _))) => Some(focus + i)
           case _ => None
-        }).iterator.map(_.info))
+        }))
 
   def entity_focus(range: Text.Range, visible_defs: Rendering.Focus): Rendering.Focus =
-    Rendering.Focus.merge(
-      snapshot.cumulate[Rendering.Focus](range, Rendering.Focus.empty, Rendering.entity_elements, _ =>
+    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)
           case _ => None
-        }).iterator.map(_.info))
+        }))
 
 
   /* caret focus */