changeset 36011 | 3ff725ac13a4 |
parent 34137 | 6cc9a0cbaf55 |
child 36012 | 0614676f14d4 |
--- a/src/Pure/Thy/html.scala Mon Mar 29 01:07:01 2010 -0700 +++ b/src/Pure/Thy/html.scala Mon Mar 29 22:43:56 2010 +0200 @@ -49,7 +49,7 @@ flush() ts + elem } - val syms = Symbol.elements(txt).map(_.toString) + val syms = Symbol.iterator(txt).map(_.toString) while (syms.hasNext) { val s1 = syms.next def s2() = if (syms.hasNext) syms.next else ""