src/Pure/PIDE/rendering.scala

 
   object Focus
   {
     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])
   {
     def defined: Boolean = rep.nonEmpty

 
   val message_elements = Markup.Elements(message_pri.keySet)
   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)
 
   val meta_data_elements =
     Markup.Elements(Markup.META_TITLE, Markup.META_CREATOR, Markup.META_CONTRIBUTOR,

 
   private def entity_focus(range: Text.Range,
       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 {
                 case Markup.Entity.Def(i) if check(true, i) => Some(focus + i)
                 case Markup.Entity.Ref(i) if check(false, i) => Some(focus + i)
                 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 =
   {
     val focus_defs = entity_focus(caret_range)

   def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
   {
     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 {
                 case Markup.Entity.Def(i) if focus(i) => Some(true)
                 case Markup.Entity.Ref(i) if focus(i) => Some(true)