tuned signature;
authorwenzelm
Thu Mar 27 11:19:31 2014 +0100 (2014-03-27)
changeset 563008346b664fa7a
parent 56299 8201790fdeb9
child 56301 1da7b4c33db9
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup_tree.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Mar 27 10:43:43 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Mar 27 11:19:31 2014 +0100
     1.3 @@ -653,11 +653,11 @@
     1.4      def command_markup(version: Version, command: Command, index: Command.Markup_Index): Markup_Tree =
     1.5        Command.State.merge_markup(command_states(version, command), index)
     1.6  
     1.7 -    def markup_to_XML(version: Version, node: Node, filter: XML.Elem => Boolean): XML.Body =
     1.8 +    def markup_to_XML(version: Version, node: Node, elements: Elements): XML.Body =
     1.9        (for {
    1.10          command <- node.commands.iterator
    1.11          markup = command_markup(version, command, Command.Markup_Index.markup)
    1.12 -        tree <- markup.to_XML(command.range, command.source, filter)
    1.13 +        tree <- markup.to_XML(command.range, command.source, elements)
    1.14        } yield tree).toList
    1.15  
    1.16      // persistent user-view
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 10:43:43 2014 +0100
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 11:19:31 2014 +0100
     2.3 @@ -167,7 +167,7 @@
     2.4          ((tree ++ entry.subtree) /: entry.markup)(
     2.5            { case (t, elem) => t + Text.Info(range, elem) }) })
     2.6  
     2.7 -  def to_XML(root_range: Text.Range, text: CharSequence, filter: XML.Elem => Boolean): XML.Body =
     2.8 +  def to_XML(root_range: Text.Range, text: CharSequence, elements: Document.Elements): XML.Body =
     2.9    {
    2.10      def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
    2.11        if (start == stop) Nil
    2.12 @@ -176,7 +176,7 @@
    2.13      def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
    2.14        (body /: rev_markups) {
    2.15          case (b, elem) =>
    2.16 -          if (!filter(elem)) b
    2.17 +          if (!elements(elem.name)) b
    2.18            else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
    2.19            else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
    2.20        }
    2.21 @@ -198,9 +198,6 @@
    2.22     make_body(root_range, Nil, overlapping(root_range))
    2.23    }
    2.24  
    2.25 -  def to_XML(text: CharSequence): XML.Body =
    2.26 -    to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
    2.27 -
    2.28    def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,
    2.29      result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
    2.30    {