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