1.1 --- a/src/Pure/Thy/html.scala	Wed Aug 17 15:14:48 2011 +0200
     1.2 +++ b/src/Pure/Thy/html.scala	Wed Aug 17 16:01:27 2011 +0200
     1.3 @@ -83,13 +83,15 @@
     1.4              val s1 = syms.next
     1.5              def s2() = if (syms.hasNext) syms.next else ""
     1.6              if (s1 == "\n") add(XML.elem(BR))
     1.7 -            else if (Symbol.is_bsub_decoded(s1)) t ++= s1  // FIXME
     1.8 -            else if (Symbol.is_esub_decoded(s1)) t ++= s1  // FIXME
     1.9 -            else if (Symbol.is_bsup_decoded(s1)) t ++= s1  // FIXME
    1.10 -            else if (Symbol.is_esup_decoded(s1)) t ++= s1  // FIXME
    1.11 -            else if (Symbol.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
    1.12 -            else if (Symbol.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
    1.13 -            else if (Symbol.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) }
    1.14 +            else if (s1 == Symbol.sub_decoded || s1 == Symbol.isub_decoded)
    1.15 +              { add(hidden(s1)); add(sub(s2())) }
    1.16 +            else if (s1 == Symbol.sup_decoded || s1 == Symbol.isup_decoded)
    1.17 +              { add(hidden(s1)); add(sup(s2())) }
    1.18 +            else if (s1 == Symbol.bsub_decoded) t ++= s1  // FIXME
    1.19 +            else if (s1 == Symbol.esub_decoded) t ++= s1  // FIXME
    1.20 +            else if (s1 == Symbol.bsup_decoded) t ++= s1  // FIXME
    1.21 +            else if (s1 == Symbol.esup_decoded) t ++= s1  // FIXME
    1.22 +            else if (s1 == Symbol.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
    1.23              else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) }
    1.24              else t ++= s1
    1.25            }