renamed DOM to document, add xml version and optional stylesheets;
authorwenzelm
Sat, 23 Aug 2008 11:48:52 +0200
changeset 27948 2638b611d3ce
parent 27947 b6dc0a396857
child 27949 6eb0327c0b9b
renamed DOM to document, add xml version and optional stylesheets;
src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Fri Aug 22 21:25:19 2008 +0200
+++ b/src/Pure/General/xml.scala	Sat Aug 23 11:48:52 2008 +0200
@@ -49,8 +49,16 @@
 
   /* document object model (DOM) */
 
-  def DOM(tree: Tree) = {
+  def document(tree: Tree, styles: String*) = {
     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\""))
+    }
+
+    // main body
     def dom_tree(tr: Tree): Node = tr match {
       case Elem(name, atts, ts) => {
         val node = doc.createElement(name)
@@ -67,5 +75,4 @@
     doc.appendChild(root_elem)
     doc
   }
-
 }