--- 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 */
--- 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)