changeset 34046 | 8e743ca417b9 |
parent 34006 | bbd146caa6b2 |
child 34137 | 6cc9a0cbaf55 |
--- 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