--- a/src/Pure/General/xml.scala Sun Dec 06 23:25:27 2009 +0100
+++ b/src/Pure/General/xml.scala Mon Dec 07 00:02:07 2009 +0100
@@ -33,31 +33,34 @@
/* string representation */
private def append_text(text: String, s: StringBuilder) {
- for (c <- text.elements) c match {
- case '<' => s.append("<")
- case '>' => s.append(">")
- case '&' => s.append("&")
- case '"' => s.append(""")
- case '\'' => s.append("'")
- case _ => s.append(c)
+ if (text == null) s ++ text
+ else {
+ for (c <- text.elements) c match {
+ case '<' => s ++ "<"
+ case '>' => s ++ ">"
+ case '&' => s ++ "&"
+ case '"' => s ++ """
+ case '\'' => s ++ "'"
+ case _ => s + c
+ }
}
}
private def append_elem(name: String, atts: Attributes, s: StringBuilder) {
- s.append(name)
+ s ++ name
for ((a, x) <- atts) {
- s.append(" "); s.append(a); s.append("=\""); append_text(x, s); s.append("\"")
+ s ++ " "; s ++ a; s ++ "=\""; append_text(x, s); s ++ "\""
}
}
private def append_tree(tree: Tree, s: StringBuilder) {
tree match {
case Elem(name, atts, Nil) =>
- s.append("<"); append_elem(name, atts, s); s.append("/>")
+ s ++ "<"; append_elem(name, atts, s); s ++ "/>"
case Elem(name, atts, ts) =>
- s.append("<"); append_elem(name, atts, s); s.append(">")
+ s ++ "<"; append_elem(name, atts, s); s ++ ">"
for (t <- ts) append_tree(t, s)
- s.append("</"); s.append(name); s.append(">")
+ s ++ "</"; s ++ name; s ++ ">"
case Text(text) => append_text(text, s)
}
}