eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);

--- a/src/Pure/PIDE/markup_tree.scala	Fri Feb 21 15:48:04 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Fri Feb 21 16:14:35 2014 +0100
@@ -38,45 +38,16 @@
 
   /* tree building blocks */
 
-  object Elements
-  {
-    val empty = new Elements(Set.empty)
-  }
-
-  final class Elements private(private val rep: Set[String])
-  {
-    def exists(pred: String => Boolean): Boolean = rep.exists(pred)
-
-    def + (name: String): Elements =
-      if (rep(name)) this
-      else new Elements(rep + name)
-
-    def + (elem: XML.Elem): Elements = this + elem.markup.name
-    def ++ (elems: Iterable[XML.Elem]): Elements = (this /: elems.iterator)(_ + _)
-
-    def ++ (other: Elements): Elements =
-      if (this eq other) this
-      else if (rep.isEmpty) other
-      else (this /: other.rep)(_ + _)
-  }
-
   object Entry
   {
     def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
-      Entry(markup.range, List(markup.info), Elements.empty + markup.info,
-        subtree, subtree.make_elements)
-
-    def apply(range: Text.Range, rev_markups: List[XML.Elem], subtree: Markup_Tree): Entry =
-      Entry(range, rev_markups, Elements.empty ++ rev_markups,
-        subtree, subtree.make_elements)
+      Entry(markup.range, List(markup.info), subtree)
   }
 
   sealed case class Entry(
     range: Text.Range,
     rev_markup: List[XML.Elem],
-    elements: Elements,
-    subtree: Markup_Tree,
-    subtree_elements: Elements)
+    subtree: Markup_Tree)
   {
     def markup: List[XML.Elem] = rev_markup.reverse
 
@@ -88,11 +59,8 @@
       result.toList
     }
 
-    def + (markup: Text.Markup): Entry =
-      copy(rev_markup = markup.info :: rev_markup, elements = elements + markup.info)
-
-    def \ (markup: Text.Markup): Entry =
-      copy(subtree = subtree + markup, subtree_elements = subtree_elements + markup.info)
+    def + (markup: Text.Markup): Entry = copy(rev_markup = markup.info :: rev_markup)
+    def \ (markup: Text.Markup): Entry = copy(subtree = subtree + markup)
   }
 
   object Branches
@@ -162,10 +130,6 @@
     }
   }
 
-  def make_elements: Elements =
-    (Elements.empty /: branches)(
-      { case (elements, (_, entry)) => elements ++ entry.subtree_elements ++ entry.elements })
-
   def + (new_markup: Text.Markup): Markup_Tree =
   {
     val new_range = new_markup.range
@@ -251,13 +215,10 @@
       stack match {
         case (parent, (range, entry) :: more) :: rest =>
           val subrange = range.restrict(root_range)
-          val subtree =
-            if (entry.subtree_elements.exists(elements))
-              entry.subtree.overlapping(subrange).toList
-            else Nil
+          val subtree = entry.subtree.overlapping(subrange).toList
           val start = subrange.start
 
-          (if (entry.elements.exists(elements)) results(parent.info, entry) else None) match {
+          results(parent.info, entry) match {
             case Some(res) =>
               val next = Text.Info(subrange, res)
               val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest)