# HG changeset patch
# User wenzelm
# Date 1219484932 -7200
# Node ID 2638b611d3ce871b2cb3657c35fa33d153b2558e
# Parent  b6dc0a396857b475b10a4f90ceb49a57e642521d
renamed DOM to document, add xml version and optional stylesheets;

diff -r b6dc0a396857 -r 2638b611d3ce 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
   }
-
 }