--- a/src/Pure/General/xml.scala Fri Dec 18 12:10:52 2009 +0100
+++ b/src/Pure/General/xml.scala Fri Dec 18 12:28:50 2009 +0100
@@ -171,21 +171,4 @@
}
DOM(tree)
}
-
- def document(tree: Tree, styles: String*): Document =
- {
- val doc = DocumentBuilderFactory.newInstance.newDocumentBuilder.newDocument
- doc.appendChild(doc.createProcessingInstruction("xml", "version=\"1.0\""))
-
- for (style <- styles) {
- doc.appendChild(doc.createProcessingInstruction("xml-stylesheet",
- "href=\"" + style + "\" type=\"text/css\""))
- }
- val root_elem = tree match {
- case Elem(_, _, _) => document_node(doc, tree)
- case Text(_) => document_node(doc, (Elem(Markup.ROOT, Nil, List(tree))))
- }
- doc.appendChild(root_elem)
- doc
- }
}