tuned;

--- a/src/Pure/General/xml.scala	Mon Dec 29 22:20:04 2008 +0100
+++ b/src/Pure/General/xml.scala	Mon Dec 29 22:36:56 2008 +0100
@@ -16,13 +16,15 @@
 
   type Attributes = List[(String, String)]
 
-  abstract class Tree
-  case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree {
-    override def toString = append_tree(this, new StringBuilder).toString
+  abstract class Tree {
+    override def toString = {
+      val s = new StringBuilder
+      append_tree(this, s)
+      s.toString
+    }
   }
-  case class Text(content: String) extends Tree {
-    override def toString = append_tree(this, new StringBuilder).toString
-  }
+  case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree
+  case class Text(content: String) extends Tree
 
 
   /* string representation */
@@ -34,7 +36,7 @@
       case '&' => s.append("&")
       case '"' => s.append(""")
       case '\'' => s.append("'")
-      case _   => s.append(c)
+      case _ => s.append(c)
     }
   }
 
@@ -45,7 +47,7 @@
     }
   }
 
-  private def append_tree(tree: Tree, s: StringBuilder): StringBuilder = {
+  private def append_tree(tree: Tree, s: StringBuilder) {
     tree match {
       case Elem(name, atts, Nil) =>
         s.append("<"); append_elem(name, atts, s); s.append("/>")
@@ -55,7 +57,6 @@
         s.append("</"); s.append(name); s.append(">")
       case Text(text) => append_text(text, s)
     }
-    s
   }