# HG changeset patch
# User wenzelm
# Date 1260449031 -3600
# Node ID 8e743ca417b9014fd9cfa240eb5c6f51bf000143
# Parent  bc71778a327de8ce0eac87d2f057c271d1a013b6
sealed XML.Tree;
keep original XML.Tree within DOM as user data;

diff -r bc71778a327d -r 8e743ca417b9 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Wed Dec 09 21:55:14 2009 +0100
+++ b/src/Pure/General/markup.scala	Thu Dec 10 13:43:51 2009 +0100
@@ -185,6 +185,6 @@
   /* content */
 
   val ROOT = "root"
-  val RAW = "raw"
   val BAD = "bad"
+  val DATA = "data"
 }
diff -r bc71778a327d -r 8e743ca417b9 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Wed Dec 09 21:55:14 2009 +0100
+++ b/src/Pure/General/xml.scala	Thu Dec 10 13:43:51 2009 +0100
@@ -16,7 +16,7 @@
 
   type Attributes = List[(String, String)]
 
-  abstract class Tree {
+  sealed abstract class Tree {
     override def toString = {
       val s = new StringBuilder
       append_tree(this, s)
@@ -97,12 +97,17 @@
   def document_node(doc: Document, tree: Tree): Node =
   {
     def DOM(tr: Tree): Node = tr match {
-      case Elem(name, atts, ts) => {
+      case Elem(Markup.DATA, Nil, List(data, t)) =>
+        val node = DOM(t)
+        node.setUserData(Markup.DATA, data, null)
+        node
+      case Elem(name, atts, ts) =>
+        if (name == Markup.DATA)
+          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)
diff -r bc71778a327d -r 8e743ca417b9 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Wed Dec 09 21:55:14 2009 +0100
+++ b/src/Pure/Thy/html.scala	Thu Dec 10 13:43:51 2009 +0100
@@ -34,7 +34,8 @@
 
   def spans(tree: XML.Tree): List[XML.Tree] =
     tree match {
-      case XML.Elem(name, _, ts) => List(span(name, ts.flatMap(spans)))
+      case XML.Elem(name, _, ts) =>
+        List(XML.elem(Markup.DATA, List(tree, span(name, ts.flatMap(spans)))))
       case XML.Text(txt) =>
         val ts = new ListBuffer[XML.Tree]
         val t = new StringBuilder