--- a/src/Pure/Thy/html.scala Sun Dec 06 23:06:53 2009 +0100
+++ b/src/Pure/Thy/html.scala Sun Dec 06 23:08:43 2009 +0100
@@ -23,29 +23,49 @@
// document markup
+ def span(cls: String, body: List[XML.Tree]): XML.Elem =
+ XML.Elem(SPAN, List((CLASS, cls)), body)
+
+ def hidden(txt: String): XML.Elem =
+ span(Markup.HIDDEN, List(XML.Text(txt)))
+
+ def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
+ def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
+
def spans(tree: XML.Tree): List[XML.Tree] =
tree match {
- case XML.Elem(name, _, ts) =>
- List(XML.Elem(SPAN, List((CLASS, name)), ts.flatMap(spans)))
+ case XML.Elem(name, _, ts) => List(span(name, ts.flatMap(spans)))
case XML.Text(txt) =>
val ts = new ListBuffer[XML.Tree]
val t = new StringBuilder
- def flush_text() {
+ def flush() {
if (!t.isEmpty) {
ts + XML.Text(t.toString)
t.clear
}
}
- for (sym <- Symbol.elements(txt)) {
- sym match {
- case "\n" =>
- flush_text()
- ts + XML.elem(BR)
- case _ =>
- t ++ sym.toString
+ def add(elem: XML.Tree) {
+ flush()
+ ts + elem
+ }
+ val syms = Symbol.elements(txt)
+ while (syms.hasNext) {
+ val s1 = syms.next
+ lazy val s2 = if (syms.hasNext) syms.next else ""
+ s1 match {
+ case "\n" => add(XML.elem(BR))
+ case "\\<^bsub>" => t ++ s1 // FIXME
+ case "\\<^esub>" => t ++ s1 // FIXME
+ case "\\<^bsup>" => t ++ s1 // FIXME
+ case "\\<^esup>" => t ++ s1 // FIXME
+ case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2))
+ case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2))
+ case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2))))
+ case "\\<^loc>" => add(hidden(s2)); add(span("loc", List(XML.Text(s2))))
+ case _ => t ++ s1
}
}
- flush_text()
+ flush()
ts.toList
}
}