src/Pure/Thy/html.scala

--- a/src/Pure/Thy/html.scala	Thu Jan 03 15:13:11 2013 +0100
+++ b/src/Pure/Thy/html.scala	Thu Jan 03 20:42:18 2013 +0100
@@ -1,7 +1,7 @@
 /*  Title:      Pure/Thy/html.scala
     Author:     Makarius
 
-Basic HTML output.
+HTML presentation elements.
 */
 
 package isabelle
@@ -29,75 +29,19 @@
   }
 
 
-  /// FIXME unused stuff
-
-  // common elements and attributes
-
-  val BODY = "body"
-  val DIV = "div"
-  val SPAN = "span"
-  val BR = "br"
-  val PRE = "pre"
-  val CLASS = "class"
-  val STYLE = "style"
-
+  // common markup elements
 
-  // document markup
-
-  def span(cls: String, body: XML.Body): XML.Elem =
-    XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
-
-  def user_font(font: String, txt: String): XML.Elem =
-    XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))
-
-  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 bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt)))
+  def session_entry(name: String): String =
+    XML.string_of_tree(
+      XML.elem("li",
+        List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),
+          List(XML.Text(name)))))) + "\n"
 
-  def spans(input: XML.Tree): XML.Body =
-  {
-    def html_spans(tree: XML.Tree): XML.Body =
-      tree match {
-        case XML.Wrapped_Elem(markup, _, ts) =>
-          List(span(markup.name, ts.flatMap(html_spans)))
-        case XML.Elem(markup, ts) =>
-          List(span(markup.name, ts.flatMap(html_spans)))
-        case XML.Text(txt) =>
-          val ts = new ListBuffer[XML.Tree]
-          val t = new StringBuilder
-          def flush() {
-            if (!t.isEmpty) {
-              ts += XML.Text(t.toString)
-              t.clear
-            }
-          }
-          def add(elem: XML.Tree) {
-            flush()
-            ts += elem
-          }
-          val syms = Symbol.iterator(txt)
-          while (syms.hasNext) {
-            val s1 = syms.next
-            def s2() = if (syms.hasNext) syms.next else ""
-            if (s1 == "\n") add(XML.elem(BR))
-            else if (s1 == Symbol.sub_decoded || s1 == Symbol.isub_decoded)
-              { add(hidden(s1)); add(sub(s2())) }
-            else if (s1 == Symbol.sup_decoded || s1 == Symbol.isup_decoded)
-              { add(hidden(s1)); add(sup(s2())) }
-            else if (s1 == Symbol.bsub_decoded) t ++= s1  // FIXME
-            else if (s1 == Symbol.esub_decoded) t ++= s1  // FIXME
-            else if (s1 == Symbol.bsup_decoded) t ++= s1  // FIXME
-            else if (s1 == Symbol.esup_decoded) t ++= s1  // FIXME
-            else if (s1 == Symbol.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
-            else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) }
-            else t ++= s1
-          }
-          flush()
-          ts.toList
-      }
-    html_spans(input)
-  }
+  def session_entries(names: List[String]): String =
+    if (names.isEmpty) "</ul>"
+    else
+      "</ul>\n</div>\n<div class=\"sessions\">\n" +
+      "<h2>Sessions</h2>\n<ul>\n" + names.map(session_entry).mkString + "</ul>";
+
+  val end_document = "\n</div>\n</body>\n</html>\n"
 }