src/Pure/Thy/html.scala
author wenzelm
Wed Aug 17 16:01:27 2011 +0200 (2011-08-17 ago)
changeset 44238 36120feb70ed
parent 43695 5130dfe1b7be
child 45666 d83797ef0d2d
permissions -rw-r--r--
some convenience actions/shortcuts for control symbols;
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@37200
    14
  // encode text
wenzelm@37200
    15
wenzelm@37200
    16
  def encode(text: String): String =
wenzelm@37200
    17
  {
wenzelm@37200
    18
    val s = new StringBuilder
wenzelm@37200
    19
    for (c <- text.iterator) c match {
wenzelm@37200
    20
      case '<' => s ++= "&lt;"
wenzelm@37200
    21
      case '>' => s ++= "&gt;"
wenzelm@37200
    22
      case '&' => s ++= "&amp;"
wenzelm@37200
    23
      case '"' => s ++= "&quot;"
wenzelm@37200
    24
      case '\'' => s ++= "&#39;"
wenzelm@37200
    25
      case '\n' => s ++= "<br/>"
wenzelm@37200
    26
      case _ => s += c
wenzelm@37200
    27
    }
wenzelm@37200
    28
    s.toString
wenzelm@37200
    29
  }
wenzelm@37200
    30
wenzelm@37200
    31
wenzelm@33984
    32
  // common elements and attributes
wenzelm@33984
    33
wenzelm@33984
    34
  val BODY = "body"
wenzelm@33984
    35
  val DIV = "div"
wenzelm@33984
    36
  val SPAN = "span"
wenzelm@33984
    37
  val BR = "br"
wenzelm@34000
    38
  val PRE = "pre"
wenzelm@33984
    39
  val CLASS = "class"
wenzelm@43490
    40
  val STYLE = "style"
wenzelm@33984
    41
wenzelm@33984
    42
wenzelm@33984
    43
  // document markup
wenzelm@33984
    44
wenzelm@38573
    45
  def span(cls: String, body: XML.Body): XML.Elem =
wenzelm@38230
    46
    XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
wenzelm@34002
    47
wenzelm@43490
    48
  def user_font(font: String, txt: String): XML.Elem =
wenzelm@43490
    49
    XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))
wenzelm@43490
    50
wenzelm@34002
    51
  def hidden(txt: String): XML.Elem =
wenzelm@34002
    52
    span(Markup.HIDDEN, List(XML.Text(txt)))
wenzelm@34002
    53
wenzelm@34002
    54
  def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
wenzelm@34002
    55
  def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
wenzelm@43459
    56
  def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt)))
wenzelm@34002
    57
wenzelm@43661
    58
  def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
wenzelm@38444
    59
  {
wenzelm@38573
    60
    def html_spans(tree: XML.Tree): XML.Body =
wenzelm@38444
    61
      tree match {
wenzelm@43548
    62
        case XML.Elem(m @ Markup(name, props), ts) =>
wenzelm@43548
    63
          val span_class =
wenzelm@43548
    64
            m match { case Markup.Entity(kind, _) => name + "_" + kind case _ => name }
wenzelm@43548
    65
          val html_span = span(span_class, ts.flatMap(html_spans))
wenzelm@43548
    66
          if (original_data) List(XML.Elem(Markup.Data, List(tree, html_span)))
wenzelm@43548
    67
          else List(html_span)
wenzelm@38444
    68
        case XML.Text(txt) =>
wenzelm@38444
    69
          val ts = new ListBuffer[XML.Tree]
wenzelm@38444
    70
          val t = new StringBuilder
wenzelm@38444
    71
          def flush() {
wenzelm@38444
    72
            if (!t.isEmpty) {
wenzelm@38444
    73
              ts += XML.Text(t.toString)
wenzelm@38444
    74
              t.clear
wenzelm@38444
    75
            }
wenzelm@34000
    76
          }
wenzelm@38444
    77
          def add(elem: XML.Tree) {
wenzelm@38444
    78
            flush()
wenzelm@38444
    79
            ts += elem
wenzelm@38444
    80
          }
wenzelm@43675
    81
          val syms = Symbol.iterator(txt)
wenzelm@38444
    82
          while (syms.hasNext) {
wenzelm@38444
    83
            val s1 = syms.next
wenzelm@38444
    84
            def s2() = if (syms.hasNext) syms.next else ""
wenzelm@43455
    85
            if (s1 == "\n") add(XML.elem(BR))
wenzelm@44238
    86
            else if (s1 == Symbol.sub_decoded || s1 == Symbol.isub_decoded)
wenzelm@44238
    87
              { add(hidden(s1)); add(sub(s2())) }
wenzelm@44238
    88
            else if (s1 == Symbol.sup_decoded || s1 == Symbol.isup_decoded)
wenzelm@44238
    89
              { add(hidden(s1)); add(sup(s2())) }
wenzelm@44238
    90
            else if (s1 == Symbol.bsub_decoded) t ++= s1  // FIXME
wenzelm@44238
    91
            else if (s1 == Symbol.esub_decoded) t ++= s1  // FIXME
wenzelm@44238
    92
            else if (s1 == Symbol.bsup_decoded) t ++= s1  // FIXME
wenzelm@44238
    93
            else if (s1 == Symbol.esup_decoded) t ++= s1  // FIXME
wenzelm@44238
    94
            else if (s1 == Symbol.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
wenzelm@43695
    95
            else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) }
wenzelm@43455
    96
            else t ++= s1
wenzelm@38444
    97
          }
wenzelm@34002
    98
          flush()
wenzelm@38444
    99
          ts.toList
wenzelm@38444
   100
      }
wenzelm@38444
   101
    html_spans(input)
wenzelm@38444
   102
  }
wenzelm@33984
   103
}