src/Pure/Thy/html.scala
changeset 43455 4b4b93672f15
parent 38573 d163f0f28e8c
child 43458 b55a273ede18
equal deleted inserted replaced
43454:71b7a535cf96 43455:4b4b93672f15
    48     span(Markup.HIDDEN, List(XML.Text(txt)))
    48     span(Markup.HIDDEN, List(XML.Text(txt)))
    49 
    49 
    50   def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
    50   def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
    51   def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
    51   def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
    52 
    52 
    53   def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
    53   def spans(symbols: Symbol.Interpretation,
       
    54     input: XML.Tree, original_data: Boolean = false): XML.Body =
    54   {
    55   {
    55     def html_spans(tree: XML.Tree): XML.Body =
    56     def html_spans(tree: XML.Tree): XML.Body =
    56       tree match {
    57       tree match {
    57         case XML.Elem(Markup(name, _), ts) =>
    58         case XML.Elem(Markup(name, _), ts) =>
    58           if (original_data)
    59           if (original_data)
    73           }
    74           }
    74           val syms = Symbol.iterator(txt).map(_.toString)
    75           val syms = Symbol.iterator(txt).map(_.toString)
    75           while (syms.hasNext) {
    76           while (syms.hasNext) {
    76             val s1 = syms.next
    77             val s1 = syms.next
    77             def s2() = if (syms.hasNext) syms.next else ""
    78             def s2() = if (syms.hasNext) syms.next else ""
    78             s1 match {
    79             if (s1 == "\n") add(XML.elem(BR))
    79               case "\n" => add(XML.elem(BR))
    80             else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
    80               case "\\<^bsub>" => t ++= s1  // FIXME
    81             else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
    81               case "\\<^esub>" => t ++= s1  // FIXME
    82             else if (s1 == "\\<^bsub>") t ++= s1  // FIXME
    82               case "\\<^bsup>" => t ++= s1  // FIXME
    83             else if (s1 == "\\<^esub>") t ++= s1  // FIXME
    83               case "\\<^esup>" => t ++= s1  // FIXME
    84             else if (s1 == "\\<^bsup>") t ++= s1  // FIXME
    84               case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
    85             else if (s1 == "\\<^esup>") t ++= s1  // FIXME
    85               case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
    86             else if (symbols.is_bold_decoded(s1)) {
    86               case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
    87               add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
    87               case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
       
    88               case _ => t ++= s1
       
    89             }
    88             }
       
    89             else if (s1 == "\\<^loc>") { add(hidden(s1)); add(span("loc", List(XML.Text(s2())))) }
       
    90             else t ++= s1
    90           }
    91           }
    91           flush()
    92           flush()
    92           ts.toList
    93           ts.toList
    93       }
    94       }
    94     html_spans(input)
    95     html_spans(input)