# HG changeset patch
# User wenzelm
# Date 1348838749 -7200
# Node ID 5a0817ec03145129a003c078a21f8ed916432d17
# Parent  343bfcbad2ecfb040a4501d48c38c5d424cbadd6
tuned signature;

diff -r 343bfcbad2ec -r 5a0817ec0314 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Sep 28 15:05:16 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Sep 28 15:25:49 2012 +0200
@@ -23,7 +23,8 @@
     val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
     val markup: Markup_Tree = Markup_Tree.empty)
   {
-    def markup_to_XML: XML.Body = markup.to_XML(command.source)
+    def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
+      markup.to_XML(command.range, command.source, filter)
 
 
     /* accumulate content */
diff -r 343bfcbad2ec -r 5a0817ec0314 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Sep 28 15:05:16 2012 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Sep 28 15:25:49 2012 +0200
@@ -478,6 +478,8 @@
       }
     }
 
+    def markup_to_XML(version: Version, node: Node, filter: XML.Elem => Boolean): XML.Body =
+      node.commands.toList.map(cmd => command_state(version, cmd).markup_to_XML(filter)).flatten
 
     // persistent user-view
     def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil)