--- a/src/Pure/PIDE/document.scala Thu Mar 27 10:43:43 2014 +0100
+++ b/src/Pure/PIDE/document.scala Thu Mar 27 11:19:31 2014 +0100
@@ -653,11 +653,11 @@
def command_markup(version: Version, command: Command, index: Command.Markup_Index): Markup_Tree =
Command.State.merge_markup(command_states(version, command), index)
- def markup_to_XML(version: Version, node: Node, filter: XML.Elem => Boolean): XML.Body =
+ def markup_to_XML(version: Version, node: Node, elements: Elements): XML.Body =
(for {
command <- node.commands.iterator
markup = command_markup(version, command, Command.Markup_Index.markup)
- tree <- markup.to_XML(command.range, command.source, filter)
+ tree <- markup.to_XML(command.range, command.source, elements)
} yield tree).toList
// persistent user-view
--- a/src/Pure/PIDE/markup_tree.scala Thu Mar 27 10:43:43 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Thu Mar 27 11:19:31 2014 +0100
@@ -167,7 +167,7 @@
((tree ++ entry.subtree) /: entry.markup)(
{ case (t, elem) => t + Text.Info(range, elem) }) })
- def to_XML(root_range: Text.Range, text: CharSequence, filter: XML.Elem => Boolean): XML.Body =
+ def to_XML(root_range: Text.Range, text: CharSequence, elements: Document.Elements): XML.Body =
{
def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
if (start == stop) Nil
@@ -176,7 +176,7 @@
def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
(body /: rev_markups) {
case (b, elem) =>
- if (!filter(elem)) b
+ if (!elements(elem.name)) b
else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
}
@@ -198,9 +198,6 @@
make_body(root_range, Nil, overlapping(root_range))
}
- def to_XML(text: CharSequence): XML.Body =
- to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
-
def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,
result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
{