# HG changeset patch
# User wenzelm
# Date 1281457392 -7200
# Node ID 11c2b8d1fde04b61099b35a059787f976931f47d
# Parent  bb2df73fab2c7e8a7a0a2dcceb2eac57cd64e475
tuned;

diff -r bb2df73fab2c -r 11c2b8d1fde0 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Tue Aug 10 15:12:45 2010 +0200
+++ b/src/Pure/General/xml.scala	Tue Aug 10 18:23:12 2010 +0200
@@ -47,14 +47,16 @@
     }
   }
 
-  private def append_elem(name: String, atts: Attributes, s: StringBuilder) {
+  private def append_elem(name: String, atts: Attributes, s: StringBuilder)
+  {
     s ++= name
     for ((a, x) <- atts) {
       s ++= " "; s ++= a; s ++= "=\""; append_text(x, s); s ++= "\""
     }
   }
 
-  private def append_tree(tree: Tree, s: StringBuilder) {
+  private def append_tree(tree: Tree, s: StringBuilder)
+  {
     tree match {
       case Elem(Markup(name, atts), Nil) =>
         s ++= "<"; append_elem(name, atts, s); s ++= "/>"