# 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)