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