# HG changeset patch
# User wenzelm
# Date 1259932867 -3600
# Node ID 5e865ed883138819256ba1cfe893a6eac8073856
# Parent  5e9ddf000d97b86ef5d40a1a0e874bebe0e8f503
added document_node;
tuned comments;

diff -r 5e9ddf000d97 -r 5e865ed88313 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Fri Dec 04 12:17:38 2009 +0100
+++ b/src/Pure/General/xml.scala	Fri Dec 04 14:21:07 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