src/Pure/PIDE/markup_tree.scala
changeset 56300 8346b664fa7a
parent 56299 8201790fdeb9
child 56301 1da7b4c33db9
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 10:43:43 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 11:19:31 2014 +0100
     1.3 @@ -167,7 +167,7 @@
     1.4          ((tree ++ entry.subtree) /: entry.markup)(
     1.5            { case (t, elem) => t + Text.Info(range, elem) }) })
     1.6  
     1.7 -  def to_XML(root_range: Text.Range, text: CharSequence, filter: XML.Elem => Boolean): XML.Body =
     1.8 +  def to_XML(root_range: Text.Range, text: CharSequence, elements: Document.Elements): XML.Body =
     1.9    {
    1.10      def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
    1.11        if (start == stop) Nil
    1.12 @@ -176,7 +176,7 @@
    1.13      def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
    1.14        (body /: rev_markups) {
    1.15          case (b, elem) =>
    1.16 -          if (!filter(elem)) b
    1.17 +          if (!elements(elem.name)) b
    1.18            else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
    1.19            else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
    1.20        }
    1.21 @@ -198,9 +198,6 @@
    1.22     make_body(root_range, Nil, overlapping(root_range))
    1.23    }
    1.24  
    1.25 -  def to_XML(text: CharSequence): XML.Body =
    1.26 -    to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
    1.27 -
    1.28    def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,
    1.29      result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
    1.30    {