# HG changeset patch
# User wenzelm
# Date 1260140527 -3600
# Node ID ada5098506aff529b0fd8c85d724a6ce03513f12
# Parent  30c8746074d0ea0c9305f508a2db1ece32262764
toString: more robust handling of null;
tuned;

diff -r 30c8746074d0 -r ada5098506af src/Pure/General/xml.scala
--- 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("&lt;")
-      case '>' => s.append("&gt;")
-      case '&' => s.append("&amp;")
-      case '"' => s.append("&quot;")
-      case '\'' => s.append("&apos;")
-      case _ => s.append(c)
+    if (text == null) s ++ text
+    else {
+      for (c <- text.elements) c match {
+        case '<' => s ++ "&lt;"
+        case '>' => s ++ "&gt;"
+        case '&' => s ++ "&amp;"
+        case '"' => s ++ "&quot;"
+        case '\'' => s ++ "&apos;"
+        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)
     }
   }