# HG changeset patch
# User wenzelm
# Date 1395915571 -3600
# Node ID 8346b664fa7a59a0b88e9a6f25fb9264c43f4ac1
# Parent  8201790fdeb93c2d4ccf728df1f0784cb10fe12a
tuned signature;

diff -r 8201790fdeb9 -r 8346b664fa7a src/Pure/PIDE/document.scala
--- 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
diff -r 8201790fdeb9 -r 8346b664fa7a src/Pure/PIDE/markup_tree.scala
--- 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]] =
   {