diff -r e6a53d203362 -r 2f6986e2ef06 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Thu Sep 27 15:38:28 2012 +0200
+++ b/src/Pure/PIDE/xml.scala	Thu Sep 27 15:55:38 2012 +0200
@@ -7,7 +7,6 @@
 
 package isabelle
 
-import java.lang.System
 import java.util.WeakHashMap
 import java.lang.ref.WeakReference
 import javax.xml.parsers.DocumentBuilderFactory
@@ -171,35 +170,6 @@
 
 
 
-  /** document object model (W3C DOM) **/
-
-  def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
-    node.getUserData(Markup.Data.name) match {
-      case tree: XML.Tree => Some(tree)
-      case _ => None
-    }
-
-  def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
-  {
-    def DOM(tr: Tree): org.w3c.dom.Node = tr match {
-      case Elem(Markup.Data, List(data, t)) =>
-        val node = DOM(t)
-        node.setUserData(Markup.Data.name, data, null)
-        node
-      case Elem(Markup(name, atts), ts) =>
-        if (name == Markup.Data.name)
-          error("Malformed data element: " + tr.toString)
-        val node = doc.createElement(name)
-        for ((name, value) <- atts) node.setAttribute(name, value)
-        for (t <- ts) node.appendChild(DOM(t))
-        node
-      case Text(txt) => doc.createTextNode(txt)
-    }
-    DOM(tree)
-  }
-
-
-
   /** XML as data representation language **/
 
   class XML_Atom(s: String) extends Exception(s)