# HG changeset patch
# User wenzelm
# Date 1269902872 -7200
# Node ID 4f5c7a19ebe04f17e08d954a26663122baaab723
# Parent  6111de7c916a157e2c4af7e8bd6af10cb22be458
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;

diff -r 6111de7c916a -r 4f5c7a19ebe0 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Tue Mar 30 00:13:27 2010 +0200
+++ b/src/Pure/General/xml.scala	Tue Mar 30 00:47:52 2010 +0200
@@ -34,34 +34,34 @@
   /* string representation */
 
   private def append_text(text: String, s: StringBuilder) {
-    if (text == null) s ++ text
+    if (text == null) s ++= text
     else {
       for (c <- text.iterator) c match {
-        case '<' => s ++ "&lt;"
-        case '>' => s ++ "&gt;"
-        case '&' => s ++ "&amp;"
-        case '"' => s ++ "&quot;"
-        case '\'' => s ++ "&apos;"
-        case _ => s + c
+        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 ++ name
+    s ++= name
     for ((a, x) <- atts) {
-      s ++ " "; s ++ a; s ++ "=\""; append_text(x, s); s ++ "\""
+      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_elem(name, atts, s); s ++ "/>"
+        s ++= "<"; append_elem(name, atts, s); s ++= "/>"
       case Elem(name, atts, ts) =>
-        s ++ "<"; append_elem(name, atts, s); s ++ ">"
+        s ++= "<"; append_elem(name, atts, s); s ++= ">"
         for (t <- ts) append_tree(t, s)
-        s ++ "</"; s ++ name; s ++ ">"
+        s ++= "</"; s ++= name; s ++= ">"
       case Text(text) => append_text(text, s)
     }
   }
diff -r 6111de7c916a -r 4f5c7a19ebe0 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Tue Mar 30 00:13:27 2010 +0200
+++ b/src/Pure/Thy/html.scala	Tue Mar 30 00:47:52 2010 +0200
@@ -55,15 +55,15 @@
           def s2() = if (syms.hasNext) syms.next else ""
           s1 match {
             case "\n" => add(XML.elem(BR))
-            case "\\<^bsub>" => t ++ s1  // FIXME
-            case "\\<^esub>" => t ++ s1  // FIXME
-            case "\\<^bsup>" => t ++ s1  // FIXME
-            case "\\<^esup>" => t ++ s1  // FIXME
+            case "\\<^bsub>" => t ++= s1  // FIXME
+            case "\\<^esub>" => t ++= s1  // FIXME
+            case "\\<^bsup>" => t ++= s1  // FIXME
+            case "\\<^esup>" => t ++= s1  // FIXME
             case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
             case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
             case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
             case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
-            case _ => t ++ s1
+            case _ => t ++= s1
           }
         }
         flush()