# HG changeset patch
# User wenzelm
# Date 1259936865 -3600
# Node ID 29b928d32203f73798990ba62507ddd54ec17dce
# Parent  c3b822d234f42aa59237a172e8eb26b7aef559d3# Parent  5e865ed883138819256ba1cfe893a6eac8073856
merged

diff -r c3b822d234f4 -r 29b928d32203 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Fri Dec 04 15:25:30 2009 +0100
+++ b/src/Pure/General/xml.scala	Fri Dec 04 15:27:45 2009 +0100
@@ -86,18 +86,10 @@
   }
 
 
-  /* document object model (DOM) */
-
-  def document(tree: Tree, styles: String*) = {
-    val doc = DocumentBuilderFactory.newInstance.newDocumentBuilder.newDocument
-    doc.appendChild(doc.createProcessingInstruction("xml", "version=\"1.0\""))
+  /* document object model (W3C DOM) */
 
-    for (style <- styles) {
-      doc.appendChild(doc.createProcessingInstruction("xml-stylesheet",
-        "href=\"" + style + "\" type=\"text/css\""))
-    }
-
-    // main body
+  def document_node(doc: Document, tree: Tree): Node =
+  {
     def DOM(tr: Tree): Node = tr match {
       case Elem(name, atts, ts) => {
         val node = doc.createElement(name)
@@ -107,9 +99,21 @@
       }
       case Text(txt) => doc.createTextNode(txt)
     }
+    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(_, _, _) => DOM(tree)
-      case Text(_) => DOM(Elem(Markup.ROOT, Nil, List(tree)))
+      case Elem(_, _, _) => document_node(doc, tree)
+      case Text(_) => document_node(doc, (Elem(Markup.ROOT, Nil, List(tree))))
     }
     doc.appendChild(root_elem)
     doc