src/Pure/Thy/html.scala
changeset 43455 4b4b93672f15
parent 38573 d163f0f28e8c
child 43458 b55a273ede18
     1.1 --- a/src/Pure/Thy/html.scala	Sun Jun 19 00:03:44 2011 +0200
     1.2 +++ b/src/Pure/Thy/html.scala	Sun Jun 19 14:11:06 2011 +0200
     1.3 @@ -50,7 +50,8 @@
     1.4    def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
     1.5    def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
     1.6  
     1.7 -  def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
     1.8 +  def spans(symbols: Symbol.Interpretation,
     1.9 +    input: XML.Tree, original_data: Boolean = false): XML.Body =
    1.10    {
    1.11      def html_spans(tree: XML.Tree): XML.Body =
    1.12        tree match {
    1.13 @@ -75,18 +76,18 @@
    1.14            while (syms.hasNext) {
    1.15              val s1 = syms.next
    1.16              def s2() = if (syms.hasNext) syms.next else ""
    1.17 -            s1 match {
    1.18 -              case "\n" => add(XML.elem(BR))
    1.19 -              case "\\<^bsub>" => t ++= s1  // FIXME
    1.20 -              case "\\<^esub>" => t ++= s1  // FIXME
    1.21 -              case "\\<^bsup>" => t ++= s1  // FIXME
    1.22 -              case "\\<^esup>" => t ++= s1  // FIXME
    1.23 -              case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
    1.24 -              case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
    1.25 -              case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
    1.26 -              case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
    1.27 -              case _ => t ++= s1
    1.28 +            if (s1 == "\n") add(XML.elem(BR))
    1.29 +            else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
    1.30 +            else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
    1.31 +            else if (s1 == "\\<^bsub>") t ++= s1  // FIXME
    1.32 +            else if (s1 == "\\<^esub>") t ++= s1  // FIXME
    1.33 +            else if (s1 == "\\<^bsup>") t ++= s1  // FIXME
    1.34 +            else if (s1 == "\\<^esup>") t ++= s1  // FIXME
    1.35 +            else if (symbols.is_bold_decoded(s1)) {
    1.36 +              add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
    1.37              }
    1.38 +            else if (s1 == "\\<^loc>") { add(hidden(s1)); add(span("loc", List(XML.Text(s2())))) }
    1.39 +            else t ++= s1
    1.40            }
    1.41            flush()
    1.42            ts.toList