src/Pure/PIDE/xml.scala
changeset 49613 2f6986e2ef06
parent 49466 99ed1f422635
child 49650 9fad6480300d
     1.1 --- a/src/Pure/PIDE/xml.scala	Thu Sep 27 15:38:28 2012 +0200
     1.2 +++ b/src/Pure/PIDE/xml.scala	Thu Sep 27 15:55:38 2012 +0200
     1.3 @@ -7,7 +7,6 @@
     1.4  
     1.5  package isabelle
     1.6  
     1.7 -import java.lang.System
     1.8  import java.util.WeakHashMap
     1.9  import java.lang.ref.WeakReference
    1.10  import javax.xml.parsers.DocumentBuilderFactory
    1.11 @@ -171,35 +170,6 @@
    1.12  
    1.13  
    1.14  
    1.15 -  /** document object model (W3C DOM) **/
    1.16 -
    1.17 -  def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
    1.18 -    node.getUserData(Markup.Data.name) match {
    1.19 -      case tree: XML.Tree => Some(tree)
    1.20 -      case _ => None
    1.21 -    }
    1.22 -
    1.23 -  def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
    1.24 -  {
    1.25 -    def DOM(tr: Tree): org.w3c.dom.Node = tr match {
    1.26 -      case Elem(Markup.Data, List(data, t)) =>
    1.27 -        val node = DOM(t)
    1.28 -        node.setUserData(Markup.Data.name, data, null)
    1.29 -        node
    1.30 -      case Elem(Markup(name, atts), ts) =>
    1.31 -        if (name == Markup.Data.name)
    1.32 -          error("Malformed data element: " + tr.toString)
    1.33 -        val node = doc.createElement(name)
    1.34 -        for ((name, value) <- atts) node.setAttribute(name, value)
    1.35 -        for (t <- ts) node.appendChild(DOM(t))
    1.36 -        node
    1.37 -      case Text(txt) => doc.createTextNode(txt)
    1.38 -    }
    1.39 -    DOM(tree)
    1.40 -  }
    1.41 -
    1.42 -
    1.43 -
    1.44    /** XML as data representation language **/
    1.45  
    1.46    class XML_Atom(s: String) extends Exception(s)