added get_data;

--- a/src/Pure/General/xml.scala	Thu Dec 10 13:43:51 2009 +0100
+++ b/src/Pure/General/xml.scala	Thu Dec 10 16:11:07 2009 +0100
@@ -94,6 +94,12 @@
 
   /* document object model (W3C DOM) */
 
+  def get_data(node: Node): Option[XML.Tree] =
+    node.getUserData(Markup.DATA) match {
+      case tree: XML.Tree => Some(tree)
+      case _ => None
+    }
+
   def document_node(doc: Document, tree: Tree): Node =
   {
     def DOM(tr: Tree): Node = tr match {