src/Pure/Thy/html.scala
changeset 36012 0614676f14d4
parent 36011 3ff725ac13a4
child 36016 4f5c7a19ebe0
     1.1 --- a/src/Pure/Thy/html.scala	Mon Mar 29 22:43:56 2010 +0200
     1.2 +++ b/src/Pure/Thy/html.scala	Mon Mar 29 22:55:57 2010 +0200
     1.3 @@ -41,13 +41,13 @@
     1.4          val t = new StringBuilder
     1.5          def flush() {
     1.6            if (!t.isEmpty) {
     1.7 -            ts + XML.Text(t.toString)
     1.8 +            ts += XML.Text(t.toString)
     1.9              t.clear
    1.10            }
    1.11          }
    1.12          def add(elem: XML.Tree) {
    1.13            flush()
    1.14 -          ts + elem
    1.15 +          ts += elem
    1.16          }
    1.17          val syms = Symbol.iterator(txt).map(_.toString)
    1.18          while (syms.hasNext) {