1.1 --- a/src/Pure/PIDE/markup_tree.scala	Sat Dec 15 16:59:33 2012 +0100
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sat Dec 15 18:30:09 2012 +0100
     1.3 @@ -43,7 +43,6 @@
     1.4    object Elements
     1.5    {
     1.6      val empty = new Elements(Set.empty)
     1.7 -    def merge(es: Iterable[Elements]): Elements = (empty /: es.iterator)(_ ++ _)
     1.8    }
     1.9  
    1.10    final class Elements private(private val rep: Set[String])
    1.11 @@ -66,22 +65,28 @@
    1.12    object Entry
    1.13    {
    1.14      def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
    1.15 -      Entry(markup.range, List(markup.info), Elements.empty + markup.info, subtree)
    1.16 +      Entry(markup.range, List(markup.info), Elements.empty + markup.info,
    1.17 +        subtree, subtree.make_elements)
    1.18  
    1.19      def apply(range: Text.Range, rev_markups: List[XML.Elem], subtree: Markup_Tree): Entry =
    1.20 -      Entry(range, rev_markups, Elements.empty ++ rev_markups, subtree)
    1.21 +      Entry(range, rev_markups, Elements.empty ++ rev_markups,
    1.22 +        subtree, subtree.make_elements)
    1.23    }
    1.24  
    1.25    sealed case class Entry(
    1.26      range: Text.Range,
    1.27      rev_markup: List[XML.Elem],
    1.28      elements: Elements,
    1.29 -    subtree: Markup_Tree)
    1.30 +    subtree: Markup_Tree,
    1.31 +    subtree_elements: Elements)
    1.32    {
    1.33 -    def + (info: XML.Elem): Entry =
    1.34 -      copy(rev_markup = info :: rev_markup, elements = elements + info)
    1.35 +    def markup: List[XML.Elem] = rev_markup.reverse
    1.36  
    1.37 -    def markup: List[XML.Elem] = rev_markup.reverse
    1.38 +    def + (markup: Text.Markup): Entry =
    1.39 +      copy(rev_markup = markup.info :: rev_markup, elements = elements + markup.info)
    1.40 +
    1.41 +    def \ (markup: Text.Markup): Entry =
    1.42 +      copy(subtree = subtree + markup, subtree_elements = subtree_elements + markup.info)
    1.43    }
    1.44  
    1.45    object Branches
    1.46 @@ -148,6 +153,10 @@
    1.47      }
    1.48    }
    1.49  
    1.50 +  def make_elements: Elements =
    1.51 +    (Elements.empty /: branches)(
    1.52 +      { case (elements, (_, entry)) => elements ++ entry.subtree_elements ++ entry.elements })
    1.53 +
    1.54    def + (new_markup: Text.Markup): Markup_Tree =
    1.55    {
    1.56      val new_range = new_markup.range
    1.57 @@ -156,9 +165,9 @@
    1.58        case None => new Markup_Tree(branches, Entry(new_markup, empty))
    1.59        case Some(entry) =>
    1.60          if (entry.range == new_range)
    1.61 -          new Markup_Tree(branches, entry + new_markup.info)
    1.62 +          new Markup_Tree(branches, entry + new_markup)
    1.63          else if (entry.range.contains(new_range))
    1.64 -          new Markup_Tree(branches, entry.copy(subtree = entry.subtree + new_markup))
    1.65 +          new Markup_Tree(branches, entry \ new_markup)
    1.66          else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
    1.67            new Markup_Tree(Branches.empty, Entry(new_markup, this))
    1.68          else {
    1.69 @@ -218,19 +227,18 @@
    1.70        }
    1.71  
    1.72      def results(x: A, entry: Entry): Option[A] =
    1.73 -      if (notable(entry.elements)) {
    1.74 -        val (y, changed) =
    1.75 -          // FIXME proper cumulation order (including status markup) (!?)
    1.76 -          ((x, false) /: entry.rev_markup)((res, info) =>
    1.77 -            {
    1.78 -              val (y, changed) = res
    1.79 -              val arg = (y, Text.Info(entry.range, info))
    1.80 -              if (result.isDefinedAt(arg)) (result(arg), true)
    1.81 -              else res
    1.82 -            })
    1.83 -        if (changed) Some(y) else None
    1.84 -      }
    1.85 -      else None
    1.86 +    {
    1.87 +      val (y, changed) =
    1.88 +        // FIXME proper cumulation order (including status markup) (!?)
    1.89 +        ((x, false) /: entry.rev_markup)((res, info) =>
    1.90 +          {
    1.91 +            val (y, changed) = res
    1.92 +            val arg = (y, Text.Info(entry.range, info))
    1.93 +            if (result.isDefinedAt(arg)) (result(arg), true)
    1.94 +            else res
    1.95 +          })
    1.96 +      if (changed) Some(y) else None
    1.97 +    }
    1.98  
    1.99      def stream(
   1.100        last: Text.Offset,
   1.101 @@ -239,10 +247,13 @@
   1.102        stack match {
   1.103          case (parent, (range, entry) #:: more) :: rest =>
   1.104            val subrange = range.restrict(root_range)
   1.105 -          val subtree = entry.subtree.overlapping(subrange).toStream
   1.106 +          val subtree =
   1.107 +            if (notable(entry.subtree_elements))
   1.108 +              entry.subtree.overlapping(subrange).toStream
   1.109 +            else Stream.empty
   1.110            val start = subrange.start
   1.111  
   1.112 -          results(parent.info, entry) match {
   1.113 +          (if (notable(entry.elements)) results(parent.info, entry) else None) match {
   1.114              case Some(res) =>
   1.115                val next = Text.Info(subrange, res)
   1.116                val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)