tuned signature;
authorwenzelm
Fri Sep 28 15:25:49 2012 +0200 (2012-09-28 ago)
changeset 496455a0817ec0314
parent 49644 343bfcbad2ec
child 49646 77a0a53caa2f
tuned signature;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Fri Sep 28 15:05:16 2012 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Fri Sep 28 15:25:49 2012 +0200
     1.3 @@ -23,7 +23,8 @@
     1.4      val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
     1.5      val markup: Markup_Tree = Markup_Tree.empty)
     1.6    {
     1.7 -    def markup_to_XML: XML.Body = markup.to_XML(command.source)
     1.8 +    def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
     1.9 +      markup.to_XML(command.range, command.source, filter)
    1.10  
    1.11  
    1.12      /* accumulate content */
     2.1 --- a/src/Pure/PIDE/document.scala	Fri Sep 28 15:05:16 2012 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Fri Sep 28 15:25:49 2012 +0200
     2.3 @@ -478,6 +478,8 @@
     2.4        }
     2.5      }
     2.6  
     2.7 +    def markup_to_XML(version: Version, node: Node, filter: XML.Elem => Boolean): XML.Body =
     2.8 +      node.commands.toList.map(cmd => command_state(version, cmd).markup_to_XML(filter)).flatten
     2.9  
    2.10      // persistent user-view
    2.11      def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil)