src/Pure/PIDE/document.scala
changeset 56300 8346b664fa7a
parent 56299 8201790fdeb9
child 56301 1da7b4c33db9
     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