src/Pure/Thy/html.scala
changeset 34046 8e743ca417b9
parent 34006 bbd146caa6b2
child 34137 6cc9a0cbaf55
     1.1 --- a/src/Pure/Thy/html.scala	Wed Dec 09 21:55:14 2009 +0100
     1.2 +++ b/src/Pure/Thy/html.scala	Thu Dec 10 13:43:51 2009 +0100
     1.3 @@ -34,7 +34,8 @@
     1.4  
     1.5    def spans(tree: XML.Tree): List[XML.Tree] =
     1.6      tree match {
     1.7 -      case XML.Elem(name, _, ts) => List(span(name, ts.flatMap(spans)))
     1.8 +      case XML.Elem(name, _, ts) =>
     1.9 +        List(XML.elem(Markup.DATA, List(tree, span(name, ts.flatMap(spans)))))
    1.10        case XML.Text(txt) =>
    1.11          val ts = new ListBuffer[XML.Tree]
    1.12          val t = new StringBuilder