src/Pure/Thy/html.scala
changeset 36016 4f5c7a19ebe0
parent 36012 0614676f14d4
child 37200 0f3edc64356a
     1.1 --- a/src/Pure/Thy/html.scala	Tue Mar 30 00:13:27 2010 +0200
     1.2 +++ b/src/Pure/Thy/html.scala	Tue Mar 30 00:47:52 2010 +0200
     1.3 @@ -55,15 +55,15 @@
     1.4            def s2() = if (syms.hasNext) syms.next else ""
     1.5            s1 match {
     1.6              case "\n" => add(XML.elem(BR))
     1.7 -            case "\\<^bsub>" => t ++ s1  // FIXME
     1.8 -            case "\\<^esub>" => t ++ s1  // FIXME
     1.9 -            case "\\<^bsup>" => t ++ s1  // FIXME
    1.10 -            case "\\<^esup>" => t ++ s1  // FIXME
    1.11 +            case "\\<^bsub>" => t ++= s1  // FIXME
    1.12 +            case "\\<^esub>" => t ++= s1  // FIXME
    1.13 +            case "\\<^bsup>" => t ++= s1  // FIXME
    1.14 +            case "\\<^esup>" => t ++= s1  // FIXME
    1.15              case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
    1.16              case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
    1.17              case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
    1.18              case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
    1.19 -            case _ => t ++ s1
    1.20 +            case _ => t ++= s1
    1.21            }
    1.22          }
    1.23          flush()