src/Pure/Thy/html.scala
author wenzelm
Mon Dec 07 00:02:54 2009 +0100 (2009-12-07 ago)
changeset 34006 bbd146caa6b2
parent 34004 30c8746074d0
child 34046 8e743ca417b9
permissions -rw-r--r--
avoid lazy val with side-effects -- spurious null pointers!?
     1 /*  Title:      Pure/Thy/html.scala
     2     Author:     Makarius
     3 
     4 Basic HTML output.
     5 */
     6 
     7 package isabelle
     8 
     9 import scala.collection.mutable.ListBuffer
    10 
    11 
    12 object HTML
    13 {
    14   // common elements and attributes
    15 
    16   val BODY = "body"
    17   val DIV = "div"
    18   val SPAN = "span"
    19   val BR = "br"
    20   val PRE = "pre"
    21   val CLASS = "class"
    22 
    23 
    24   // document markup
    25 
    26   def span(cls: String, body: List[XML.Tree]): XML.Elem =
    27     XML.Elem(SPAN, List((CLASS, cls)), body)
    28 
    29   def hidden(txt: String): XML.Elem =
    30     span(Markup.HIDDEN, List(XML.Text(txt)))
    31 
    32   def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
    33   def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
    34 
    35   def spans(tree: XML.Tree): List[XML.Tree] =
    36     tree match {
    37       case XML.Elem(name, _, ts) => List(span(name, ts.flatMap(spans)))
    38       case XML.Text(txt) =>
    39         val ts = new ListBuffer[XML.Tree]
    40         val t = new StringBuilder
    41         def flush() {
    42           if (!t.isEmpty) {
    43             ts + XML.Text(t.toString)
    44             t.clear
    45           }
    46         }
    47         def add(elem: XML.Tree) {
    48           flush()
    49           ts + elem
    50         }
    51         val syms = Symbol.elements(txt)
    52         while (syms.hasNext) {
    53           val s1 = syms.next
    54           def s2() = if (syms.hasNext) syms.next else ""
    55           s1 match {
    56             case "\n" => add(XML.elem(BR))
    57             case "\\<^bsub>" => t ++ s1  // FIXME
    58             case "\\<^esub>" => t ++ s1  // FIXME
    59             case "\\<^bsup>" => t ++ s1  // FIXME
    60             case "\\<^esup>" => t ++ s1  // FIXME
    61             case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
    62             case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
    63             case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
    64             case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
    65             case _ => t ++ s1
    66           }
    67         }
    68         flush()
    69         ts.toList
    70     }
    71 }