1.1 --- a/src/Pure/Thy/html.scala	Wed Jul 06 23:11:59 2011 +0200
     1.2 +++ b/src/Pure/Thy/html.scala	Thu Jul 07 13:48:30 2011 +0200
     1.3 @@ -57,8 +57,6 @@
     1.4  
     1.5    def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
     1.6    {
     1.7 -    val symbols = Isabelle_System.symbols
     1.8 -
     1.9      def html_spans(tree: XML.Tree): XML.Body =
    1.10        tree match {
    1.11          case XML.Elem(m @ Markup(name, props), ts) =>
    1.12 @@ -85,14 +83,14 @@
    1.13              val s1 = syms.next
    1.14              def s2() = if (syms.hasNext) syms.next else ""
    1.15              if (s1 == "\n") add(XML.elem(BR))
    1.16 -            else if (s1 == symbols.bsub_decoded) t ++= s1  // FIXME
    1.17 -            else if (s1 == symbols.esub_decoded) t ++= s1  // FIXME
    1.18 -            else if (s1 == symbols.bsup_decoded) t ++= s1  // FIXME
    1.19 -            else if (s1 == symbols.esup_decoded) t ++= s1  // FIXME
    1.20 -            else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
    1.21 -            else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
    1.22 -            else if (s1 == symbols.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
    1.23 -            else if (symbols.fonts.isDefinedAt(s1)) { add(user_font(symbols.fonts(s1), s1)) }
    1.24 +            else if (Symbol.is_bsub_decoded(s1)) t ++= s1  // FIXME
    1.25 +            else if (Symbol.is_esub_decoded(s1)) t ++= s1  // FIXME
    1.26 +            else if (Symbol.is_bsup_decoded(s1)) t ++= s1  // FIXME
    1.27 +            else if (Symbol.is_esup_decoded(s1)) t ++= s1  // FIXME
    1.28 +            else if (Symbol.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
    1.29 +            else if (Symbol.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
    1.30 +            else if (Symbol.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) }
    1.31 +            else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) }
    1.32              else t ++= s1
    1.33            }
    1.34            flush()