sealed XML.Tree;
authorwenzelm
Thu Dec 10 13:43:51 2009 +0100 (2009-12-10 ago)
changeset 340468e743ca417b9
parent 34045 bc71778a327d
child 34047 2af94d45597f
sealed XML.Tree;
keep original XML.Tree within DOM as user data;
src/Pure/General/markup.scala
src/Pure/General/xml.scala
src/Pure/Thy/html.scala
     1.1 --- a/src/Pure/General/markup.scala	Wed Dec 09 21:55:14 2009 +0100
     1.2 +++ b/src/Pure/General/markup.scala	Thu Dec 10 13:43:51 2009 +0100
     1.3 @@ -185,6 +185,6 @@
     1.4    /* content */
     1.5  
     1.6    val ROOT = "root"
     1.7 -  val RAW = "raw"
     1.8    val BAD = "bad"
     1.9 +  val DATA = "data"
    1.10  }
     2.1 --- a/src/Pure/General/xml.scala	Wed Dec 09 21:55:14 2009 +0100
     2.2 +++ b/src/Pure/General/xml.scala	Thu Dec 10 13:43:51 2009 +0100
     2.3 @@ -16,7 +16,7 @@
     2.4  
     2.5    type Attributes = List[(String, String)]
     2.6  
     2.7 -  abstract class Tree {
     2.8 +  sealed abstract class Tree {
     2.9      override def toString = {
    2.10        val s = new StringBuilder
    2.11        append_tree(this, s)
    2.12 @@ -97,12 +97,17 @@
    2.13    def document_node(doc: Document, tree: Tree): Node =
    2.14    {
    2.15      def DOM(tr: Tree): Node = tr match {
    2.16 -      case Elem(name, atts, ts) => {
    2.17 +      case Elem(Markup.DATA, Nil, List(data, t)) =>
    2.18 +        val node = DOM(t)
    2.19 +        node.setUserData(Markup.DATA, data, null)
    2.20 +        node
    2.21 +      case Elem(name, atts, ts) =>
    2.22 +        if (name == Markup.DATA)
    2.23 +          error("Malformed data element: " + tr.toString)
    2.24          val node = doc.createElement(name)
    2.25          for ((name, value) <- atts) node.setAttribute(name, value)
    2.26          for (t <- ts) node.appendChild(DOM(t))
    2.27          node
    2.28 -      }
    2.29        case Text(txt) => doc.createTextNode(txt)
    2.30      }
    2.31      DOM(tree)
     3.1 --- a/src/Pure/Thy/html.scala	Wed Dec 09 21:55:14 2009 +0100
     3.2 +++ b/src/Pure/Thy/html.scala	Thu Dec 10 13:43:51 2009 +0100
     3.3 @@ -34,7 +34,8 @@
     3.4  
     3.5    def spans(tree: XML.Tree): List[XML.Tree] =
     3.6      tree match {
     3.7 -      case XML.Elem(name, _, ts) => List(span(name, ts.flatMap(spans)))
     3.8 +      case XML.Elem(name, _, ts) =>
     3.9 +        List(XML.elem(Markup.DATA, List(tree, span(name, ts.flatMap(spans)))))
    3.10        case XML.Text(txt) =>
    3.11          val ts = new ListBuffer[XML.Tree]
    3.12          val t = new StringBuilder