basic treatment of special control symbols;
authorwenzelm
Sun Dec 06 23:08:43 2009 +0100 (2009-12-06 ago)
changeset 34002cbeeef3aebb3
parent 34001 6e5eafb373b3
child 34003 610e41138486
basic treatment of special control symbols;
misc tuning;
src/Pure/Thy/html.scala
     1.1 --- a/src/Pure/Thy/html.scala	Sun Dec 06 23:06:53 2009 +0100
     1.2 +++ b/src/Pure/Thy/html.scala	Sun Dec 06 23:08:43 2009 +0100
     1.3 @@ -23,29 +23,49 @@
     1.4  
     1.5    // document markup
     1.6  
     1.7 +  def span(cls: String, body: List[XML.Tree]): XML.Elem =
     1.8 +    XML.Elem(SPAN, List((CLASS, cls)), body)
     1.9 +
    1.10 +  def hidden(txt: String): XML.Elem =
    1.11 +    span(Markup.HIDDEN, List(XML.Text(txt)))
    1.12 +
    1.13 +  def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
    1.14 +  def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
    1.15 +
    1.16    def spans(tree: XML.Tree): List[XML.Tree] =
    1.17      tree match {
    1.18 -      case XML.Elem(name, _, ts) =>
    1.19 -        List(XML.Elem(SPAN, List((CLASS, name)), ts.flatMap(spans)))
    1.20 +      case XML.Elem(name, _, ts) => List(span(name, ts.flatMap(spans)))
    1.21        case XML.Text(txt) =>
    1.22          val ts = new ListBuffer[XML.Tree]
    1.23          val t = new StringBuilder
    1.24 -        def flush_text() {
    1.25 +        def flush() {
    1.26            if (!t.isEmpty) {
    1.27              ts + XML.Text(t.toString)
    1.28              t.clear
    1.29            }
    1.30          }
    1.31 -        for (sym <- Symbol.elements(txt)) {
    1.32 -          sym match {
    1.33 -            case "\n" =>
    1.34 -              flush_text()
    1.35 -              ts + XML.elem(BR)
    1.36 -            case _ =>
    1.37 -              t ++ sym.toString
    1.38 +        def add(elem: XML.Tree) {
    1.39 +          flush()
    1.40 +          ts + elem
    1.41 +        }
    1.42 +        val syms = Symbol.elements(txt)
    1.43 +        while (syms.hasNext) {
    1.44 +          val s1 = syms.next
    1.45 +          lazy val s2 = if (syms.hasNext) syms.next else ""
    1.46 +          s1 match {
    1.47 +            case "\n" => add(XML.elem(BR))
    1.48 +            case "\\<^bsub>" => t ++ s1  // FIXME
    1.49 +            case "\\<^esub>" => t ++ s1  // FIXME
    1.50 +            case "\\<^bsup>" => t ++ s1  // FIXME
    1.51 +            case "\\<^esup>" => t ++ s1  // FIXME
    1.52 +            case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2))
    1.53 +            case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2))
    1.54 +            case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2))))
    1.55 +            case "\\<^loc>" => add(hidden(s2)); add(span("loc", List(XML.Text(s2))))
    1.56 +            case _ => t ++ s1
    1.57            }
    1.58          }
    1.59 -        flush_text()
    1.60 +        flush()
    1.61          ts.toList
    1.62      }
    1.63  }