src/Pure/PIDE/markup_tree.scala
changeset 55652 33ad12ef79ff
parent 55645 561754277494
child 55820 61869776ce1f
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Fri Feb 21 15:48:04 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Fri Feb 21 16:14:35 2014 +0100
     1.3 @@ -38,45 +38,16 @@
     1.4  
     1.5    /* tree building blocks */
     1.6  
     1.7 -  object Elements
     1.8 -  {
     1.9 -    val empty = new Elements(Set.empty)
    1.10 -  }
    1.11 -
    1.12 -  final class Elements private(private val rep: Set[String])
    1.13 -  {
    1.14 -    def exists(pred: String => Boolean): Boolean = rep.exists(pred)
    1.15 -
    1.16 -    def + (name: String): Elements =
    1.17 -      if (rep(name)) this
    1.18 -      else new Elements(rep + name)
    1.19 -
    1.20 -    def + (elem: XML.Elem): Elements = this + elem.markup.name
    1.21 -    def ++ (elems: Iterable[XML.Elem]): Elements = (this /: elems.iterator)(_ + _)
    1.22 -
    1.23 -    def ++ (other: Elements): Elements =
    1.24 -      if (this eq other) this
    1.25 -      else if (rep.isEmpty) other
    1.26 -      else (this /: other.rep)(_ + _)
    1.27 -  }
    1.28 -
    1.29    object Entry
    1.30    {
    1.31      def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
    1.32 -      Entry(markup.range, List(markup.info), Elements.empty + markup.info,
    1.33 -        subtree, subtree.make_elements)
    1.34 -
    1.35 -    def apply(range: Text.Range, rev_markups: List[XML.Elem], subtree: Markup_Tree): Entry =
    1.36 -      Entry(range, rev_markups, Elements.empty ++ rev_markups,
    1.37 -        subtree, subtree.make_elements)
    1.38 +      Entry(markup.range, List(markup.info), subtree)
    1.39    }
    1.40  
    1.41    sealed case class Entry(
    1.42      range: Text.Range,
    1.43      rev_markup: List[XML.Elem],
    1.44 -    elements: Elements,
    1.45 -    subtree: Markup_Tree,
    1.46 -    subtree_elements: Elements)
    1.47 +    subtree: Markup_Tree)
    1.48    {
    1.49      def markup: List[XML.Elem] = rev_markup.reverse
    1.50  
    1.51 @@ -88,11 +59,8 @@
    1.52        result.toList
    1.53      }
    1.54  
    1.55 -    def + (markup: Text.Markup): Entry =
    1.56 -      copy(rev_markup = markup.info :: rev_markup, elements = elements + markup.info)
    1.57 -
    1.58 -    def \ (markup: Text.Markup): Entry =
    1.59 -      copy(subtree = subtree + markup, subtree_elements = subtree_elements + markup.info)
    1.60 +    def + (markup: Text.Markup): Entry = copy(rev_markup = markup.info :: rev_markup)
    1.61 +    def \ (markup: Text.Markup): Entry = copy(subtree = subtree + markup)
    1.62    }
    1.63  
    1.64    object Branches
    1.65 @@ -162,10 +130,6 @@
    1.66      }
    1.67    }
    1.68  
    1.69 -  def make_elements: Elements =
    1.70 -    (Elements.empty /: branches)(
    1.71 -      { case (elements, (_, entry)) => elements ++ entry.subtree_elements ++ entry.elements })
    1.72 -
    1.73    def + (new_markup: Text.Markup): Markup_Tree =
    1.74    {
    1.75      val new_range = new_markup.range
    1.76 @@ -251,13 +215,10 @@
    1.77        stack match {
    1.78          case (parent, (range, entry) :: more) :: rest =>
    1.79            val subrange = range.restrict(root_range)
    1.80 -          val subtree =
    1.81 -            if (entry.subtree_elements.exists(elements))
    1.82 -              entry.subtree.overlapping(subrange).toList
    1.83 -            else Nil
    1.84 +          val subtree = entry.subtree.overlapping(subrange).toList
    1.85            val start = subrange.start
    1.86  
    1.87 -          (if (entry.elements.exists(elements)) results(parent.info, entry) else None) match {
    1.88 +          results(parent.info, entry) match {
    1.89              case Some(res) =>
    1.90                val next = Text.Info(subrange, res)
    1.91                val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest)