# HG changeset patch
# User wenzelm
# Date 1348754138 -7200
# Node ID 2f6986e2ef06a758a7a3be263339b29b6636c8e2
# Parent  e6a53d203362d945c1aeb80fcd9660e5d22149e6
removed obsolete org.w3c.dom operations;

diff -r e6a53d203362 -r 2f6986e2ef06 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Thu Sep 27 15:38:28 2012 +0200
+++ b/src/Pure/PIDE/markup.scala	Thu Sep 27 15:55:38 2012 +0200
@@ -22,7 +22,6 @@
   /* elements */
 
   val Empty = Markup("", Nil)
-  val Data = Markup("data", Nil)
   val Broken = Markup("broken", Nil)
 }
 
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)
diff -r e6a53d203362 -r 2f6986e2ef06 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Thu Sep 27 15:38:28 2012 +0200
+++ b/src/Pure/Thy/html.scala	Thu Sep 27 15:55:38 2012 +0200
@@ -29,6 +29,8 @@
   }
 
 
+  /// FIXME unused stuff
+
   // common elements and attributes
 
   val BODY = "body"
@@ -55,14 +57,12 @@
   def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
   def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt)))
 
-  def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
+  def spans(input: XML.Tree): XML.Body =
   {
     def html_spans(tree: XML.Tree): XML.Body =
       tree match {
         case XML.Elem(m @ Markup(name, props), ts) =>
-          val html_span = span(name, ts.flatMap(html_spans))
-          if (original_data) List(XML.Elem(Markup.Data, List(tree, html_span)))
-          else List(html_span)
+          List(span(name, ts.flatMap(html_spans)))
         case XML.Text(txt) =>
           val ts = new ListBuffer[XML.Tree]
           val t = new StringBuilder