| changeset 34137 | 6cc9a0cbaf55 |
| parent 34046 | 8e743ca417b9 |
| child 36011 | 3ff725ac13a4 |
--- a/src/Pure/Thy/html.scala Sat Dec 19 16:02:26 2009 +0100 +++ b/src/Pure/Thy/html.scala Sat Dec 19 16:51:32 2009 +0100 @@ -49,7 +49,7 @@ flush() ts + elem } - val syms = Symbol.elements(txt) + val syms = Symbol.elements(txt).map(_.toString) while (syms.hasNext) { val s1 = syms.next def s2() = if (syms.hasNext) syms.next else ""