1.1 --- a/src/Pure/General/xml.scala	Tue Mar 30 00:13:27 2010 +0200
     1.2 +++ b/src/Pure/General/xml.scala	Tue Mar 30 00:47:52 2010 +0200
     1.3 @@ -34,34 +34,34 @@
     1.4    /* string representation */
     1.5  
     1.6    private def append_text(text: String, s: StringBuilder) {
     1.7 -    if (text == null) s ++ text
     1.8 +    if (text == null) s ++= text
     1.9      else {
    1.10        for (c <- text.iterator) c match {
    1.11 -        case '<' => s ++ "&lt;"
    1.12 -        case '>' => s ++ "&gt;"
    1.13 -        case '&' => s ++ "&amp;"
    1.14 -        case '"' => s ++ "&quot;"
    1.15 -        case '\'' => s ++ "&apos;"
    1.16 -        case _ => s + c
    1.17 +        case '<' => s ++= "&lt;"
    1.18 +        case '>' => s ++= "&gt;"
    1.19 +        case '&' => s ++= "&amp;"
    1.20 +        case '"' => s ++= "&quot;"
    1.21 +        case '\'' => s ++= "&apos;"
    1.22 +        case _ => s += c
    1.23        }
    1.24      }
    1.25    }
    1.26  
    1.27    private def append_elem(name: String, atts: Attributes, s: StringBuilder) {
    1.28 -    s ++ name
    1.29 +    s ++= name
    1.30      for ((a, x) <- atts) {
    1.31 -      s ++ " "; s ++ a; s ++ "=\""; append_text(x, s); s ++ "\""
    1.32 +      s ++= " "; s ++= a; s ++= "=\""; append_text(x, s); s ++= "\""
    1.33      }
    1.34    }
    1.35  
    1.36    private def append_tree(tree: Tree, s: StringBuilder) {
    1.37      tree match {
    1.38        case Elem(name, atts, Nil) =>
    1.39 -        s ++ "<"; append_elem(name, atts, s); s ++ "/>"
    1.40 +        s ++= "<"; append_elem(name, atts, s); s ++= "/>"
    1.41        case Elem(name, atts, ts) =>
    1.42 -        s ++ "<"; append_elem(name, atts, s); s ++ ">"
    1.43 +        s ++= "<"; append_elem(name, atts, s); s ++= ">"
    1.44          for (t <- ts) append_tree(t, s)
    1.45 -        s ++ "</"; s ++ name; s ++ ">"
    1.46 +        s ++= "</"; s ++= name; s ++= ">"
    1.47        case Text(text) => append_text(text, s)
    1.48      }
    1.49    }

     2.1 --- a/src/Pure/Thy/html.scala	Tue Mar 30 00:13:27 2010 +0200
     2.2 +++ b/src/Pure/Thy/html.scala	Tue Mar 30 00:47:52 2010 +0200
     2.3 @@ -55,15 +55,15 @@
     2.4            def s2() = if (syms.hasNext) syms.next else ""
     2.5            s1 match {
     2.6              case "\n" => add(XML.elem(BR))
     2.7 -            case "\\<^bsub>" => t ++ s1  // FIXME
     2.8 -            case "\\<^esub>" => t ++ s1  // FIXME
     2.9 -            case "\\<^bsup>" => t ++ s1  // FIXME
    2.10 -            case "\\<^esup>" => t ++ s1  // FIXME
    2.11 +            case "\\<^bsub>" => t ++= s1  // FIXME
    2.12 +            case "\\<^esub>" => t ++= s1  // FIXME
    2.13 +            case "\\<^bsup>" => t ++= s1  // FIXME
    2.14 +            case "\\<^esup>" => t ++= s1  // FIXME
    2.15              case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
    2.16              case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
    2.17              case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
    2.18              case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
    2.19 -            case _ => t ++ s1
    2.20 +            case _ => t ++= s1
    2.21            }
    2.22          }
    2.23          flush()