--- 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()