1.1 --- a/src/Pure/PIDE/markup_tree.scala	Sat Dec 15 14:45:08 2012 +0100
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sat Dec 15 16:59:33 2012 +0100
     1.3 @@ -18,6 +18,8 @@
     1.4  
     1.5  object Markup_Tree
     1.6  {
     1.7 +  /* construct trees */
     1.8 +
     1.9    val empty: Markup_Tree = new Markup_Tree(Branches.empty)
    1.10  
    1.11    def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
    1.12 @@ -35,24 +37,49 @@
    1.13            })
    1.14      }
    1.15  
    1.16 +
    1.17 +  /* tree building blocks */
    1.18 +
    1.19 +  object Elements
    1.20 +  {
    1.21 +    val empty = new Elements(Set.empty)
    1.22 +    def merge(es: Iterable[Elements]): Elements = (empty /: es.iterator)(_ ++ _)
    1.23 +  }
    1.24 +
    1.25 +  final class Elements private(private val rep: Set[String])
    1.26 +  {
    1.27 +    def contains(name: String): Boolean = rep.contains(name)
    1.28 +
    1.29 +    def + (name: String): Elements =
    1.30 +      if (contains(name)) this
    1.31 +      else new Elements(rep + name)
    1.32 +
    1.33 +    def + (elem: XML.Elem): Elements = this + elem.markup.name
    1.34 +    def ++ (elems: Iterable[XML.Elem]): Elements = (this /: elems.iterator)(_ + _)
    1.35 +
    1.36 +    def ++ (other: Elements): Elements =
    1.37 +      if (this eq other) this
    1.38 +      else if (rep.isEmpty) other
    1.39 +      else (this /: other.rep)(_ + _)
    1.40 +  }
    1.41 +
    1.42    object Entry
    1.43    {
    1.44      def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
    1.45 -      Entry(markup.range, List(markup.info), Set(markup.info.markup.name), subtree)
    1.46 +      Entry(markup.range, List(markup.info), Elements.empty + markup.info, subtree)
    1.47  
    1.48      def apply(range: Text.Range, rev_markups: List[XML.Elem], subtree: Markup_Tree): Entry =
    1.49 -      Entry(range, rev_markups, Set.empty ++ rev_markups.iterator.map(_.markup.name), subtree)
    1.50 +      Entry(range, rev_markups, Elements.empty ++ rev_markups, subtree)
    1.51    }
    1.52  
    1.53    sealed case class Entry(
    1.54      range: Text.Range,
    1.55      rev_markup: List[XML.Elem],
    1.56 -    elements: Set[String],
    1.57 +    elements: Elements,
    1.58      subtree: Markup_Tree)
    1.59    {
    1.60      def + (info: XML.Elem): Entry =
    1.61 -      if (elements(info.markup.name)) copy(rev_markup = info :: rev_markup)
    1.62 -      else copy(rev_markup = info :: rev_markup, elements = elements + info.markup.name)
    1.63 +      copy(rev_markup = info :: rev_markup, elements = elements + info)
    1.64  
    1.65      def markup: List[XML.Elem] = rev_markup.reverse
    1.66    }
    1.67 @@ -184,10 +211,17 @@
    1.68    def cumulate[A](root_range: Text.Range, root_info: A, result_elements: Option[Set[String]],
    1.69      result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
    1.70    {
    1.71 +    val notable: Elements => Boolean =
    1.72 +      result_elements match {
    1.73 +        case Some(res) => (elements: Elements) => res.exists(elements.contains)
    1.74 +        case None => (elements: Elements) => true
    1.75 +      }
    1.76 +
    1.77      def results(x: A, entry: Entry): Option[A] =
    1.78 -      if (result_elements match { case Some(es) => es.exists(entry.elements) case None => true }) {
    1.79 +      if (notable(entry.elements)) {
    1.80          val (y, changed) =
    1.81 -          ((x, false) /: entry.rev_markup)((res, info) =>  // FIXME proper order!?
    1.82 +          // FIXME proper cumulation order (including status markup) (!?)
    1.83 +          ((x, false) /: entry.rev_markup)((res, info) =>
    1.84              {
    1.85                val (y, changed) = res
    1.86                val arg = (y, Text.Info(entry.range, info))