src/Pure/Thy/html.scala
changeset 43459 def9784a3316
parent 43458 b55a273ede18
child 43489 132f99cc0a43
     1.1 --- a/src/Pure/Thy/html.scala	Sun Jun 19 15:22:58 2011 +0200
     1.2 +++ b/src/Pure/Thy/html.scala	Sun Jun 19 15:31:16 2011 +0200
     1.3 @@ -49,6 +49,7 @@
     1.4  
     1.5    def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
     1.6    def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
     1.7 +  def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt)))
     1.8  
     1.9    def spans(symbols: Symbol.Interpretation,
    1.10      input: XML.Tree, original_data: Boolean = false): XML.Body =
    1.11 @@ -77,15 +78,13 @@
    1.12              val s1 = syms.next
    1.13              def s2() = if (syms.hasNext) syms.next else ""
    1.14              if (s1 == "\n") add(XML.elem(BR))
    1.15 -            else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
    1.16 -            else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
    1.17              else if (s1 == "\\<^bsub>") t ++= s1  // FIXME
    1.18              else if (s1 == "\\<^esub>") t ++= s1  // FIXME
    1.19              else if (s1 == "\\<^bsup>") t ++= s1  // FIXME
    1.20              else if (s1 == "\\<^esup>") t ++= s1  // FIXME
    1.21 -            else if (symbols.is_bold_decoded(s1)) {
    1.22 -              add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
    1.23 -            }
    1.24 +            else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
    1.25 +            else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
    1.26 +            else if (symbols.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) }
    1.27              else t ++= s1
    1.28            }
    1.29            flush()