# HG changeset patch
# User wenzelm
# Date 1260137323 -3600
# Node ID cbeeef3aebb39c67b84557d261f8618e37a5a7ab
# Parent  6e5eafb373b38abcf0051cc5ea8f1055c3040382
basic treatment of special control symbols;
misc tuning;

diff -r 6e5eafb373b3 -r cbeeef3aebb3 src/Pure/Thy/html.scala
--- 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
     }
 }