changeset 36011 | 3ff725ac13a4 |
parent 34871 | e596a0b71f3c |
child 36016 | 4f5c7a19ebe0 |
--- a/src/Pure/General/xml.scala Mon Mar 29 01:07:01 2010 -0700 +++ b/src/Pure/General/xml.scala Mon Mar 29 22:43:56 2010 +0200 @@ -36,7 +36,7 @@ private def append_text(text: String, s: StringBuilder) { if (text == null) s ++ text else { - for (c <- text.elements) c match { + for (c <- text.iterator) c match { case '<' => s ++ "<" case '>' => s ++ ">" case '&' => s ++ "&"