# HG changeset patch
# User wenzelm
# Date 1219433119 -7200
# Node ID b6dc0a396857b475b10a4f90ceb49a57e642521d
# Parent  ec706ad3756487c6b6b003dda2b5b66b1319d97a
tuned comments;
added document object model (DOM);

diff -r ec706ad37564 -r b6dc0a396857 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Thu Aug 21 22:06:17 2008 +0200
+++ b/src/Pure/General/xml.scala	Fri Aug 22 21:25:19 2008 +0200
@@ -2,12 +2,18 @@
     ID:         $Id$
     Author:     Makarius
 
-Minimalistic XML tree values.
+Simple XML tree values.
 */
 
 package isabelle
 
+import org.w3c.dom.{Node, Document}
+import javax.xml.parsers.DocumentBuilderFactory
+
+
 object XML {
+  /* datatype representation */
+
   type Attributes = List[(String, String)]
 
   abstract class Tree
@@ -40,4 +46,26 @@
     }
   }
 
+
+  /* document object model (DOM) */
+
+  def DOM(tree: Tree) = {
+    val doc = DocumentBuilderFactory.newInstance.newDocumentBuilder.newDocument
+    def dom_tree(tr: Tree): Node = tr match {
+      case Elem(name, atts, ts) => {
+        val node = doc.createElement(name)
+        for ((name, value) <- atts) node.setAttribute(name, value)
+        for (t <- ts) node.appendChild(dom_tree(t))
+        node
+      }
+      case Text(txt) => doc.createTextNode(txt)
+    }
+    val root_elem = tree match {
+      case Elem(_, _, _) => dom_tree(tree)
+      case Text(_) => dom_tree(Elem("root", Nil, List(tree)))
+    }
+    doc.appendChild(root_elem)
+    doc
+  }
+
 }