src/Pure/Thy/html.scala
author wenzelm
Mon Mar 29 22:55:57 2010 +0200 (2010-03-29 ago)
changeset 36012 0614676f14d4
parent 36011 3ff725ac13a4
child 36016 4f5c7a19ebe0
permissions -rw-r--r--
replaced some deprecated methods;
     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) =>
    38         List(XML.elem(Markup.DATA, List(tree, span(name, ts.flatMap(spans)))))
    39       case XML.Text(txt) =>
    40         val ts = new ListBuffer[XML.Tree]
    41         val t = new StringBuilder
    42         def flush() {
    43           if (!t.isEmpty) {
    44             ts += XML.Text(t.toString)
    45             t.clear
    46           }
    47         }
    48         def add(elem: XML.Tree) {
    49           flush()
    50           ts += elem
    51         }
    52         val syms = Symbol.iterator(txt).map(_.toString)
    53         while (syms.hasNext) {
    54           val s1 = syms.next
    55           def s2() = if (syms.hasNext) syms.next else ""
    56           s1 match {
    57             case "\n" => add(XML.elem(BR))
    58             case "\\<^bsub>" => t ++ s1  // FIXME
    59             case "\\<^esub>" => t ++ s1  // FIXME
    60             case "\\<^bsup>" => t ++ s1  // FIXME
    61             case "\\<^esup>" => t ++ s1  // FIXME
    62             case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
    63             case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
    64             case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
    65             case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
    66             case _ => t ++ s1
    67           }
    68         }
    69         flush()
    70         ts.toList
    71     }
    72 }