src/Pure/PIDE/markup_tree.scala
changeset 55820 61869776ce1f
parent 55652 33ad12ef79ff
child 56299 8201790fdeb9
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Sat Mar 01 09:34:08 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sat Mar 01 12:07:26 2014 +0100
     1.3 @@ -51,10 +51,10 @@
     1.4    {
     1.5      def markup: List[XML.Elem] = rev_markup.reverse
     1.6  
     1.7 -    def filter_markup(pred: String => Boolean): List[XML.Elem] =
     1.8 +    def filter_markup(elements: Document.Elements): List[XML.Elem] =
     1.9      {
    1.10        var result: List[XML.Elem] = Nil
    1.11 -      for { elem <- rev_markup; if (pred(elem.name)) }
    1.12 +      for { elem <- rev_markup; if (elements(elem.name)) }
    1.13          result ::= elem
    1.14        result.toList
    1.15      }
    1.16 @@ -194,7 +194,7 @@
    1.17    def to_XML(text: CharSequence): XML.Body =
    1.18      to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
    1.19  
    1.20 -  def cumulate[A](root_range: Text.Range, root_info: A, elements: String => Boolean,
    1.21 +  def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,
    1.22      result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
    1.23    {
    1.24      def results(x: A, entry: Entry): Option[A] =