src/Pure/Thy/html.scala
author wenzelm
Sat Aug 07 22:09:52 2010 +0200 (2010-08-07 ago)
changeset 38230 ed147003de4b
parent 37200 0f3edc64356a
child 38231 968844caaff9
permissions -rw-r--r--
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
XML.cache_tree: actually store XML.Text as well;
added Isabelle_Process.Result.properties;
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@33984
    40
wenzelm@33984
    41
wenzelm@33984
    42
  // document markup
wenzelm@33984
    43
wenzelm@34002
    44
  def span(cls: String, body: List[XML.Tree]): XML.Elem =
wenzelm@38230
    45
    XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
wenzelm@34002
    46
wenzelm@34002
    47
  def hidden(txt: String): XML.Elem =
wenzelm@34002
    48
    span(Markup.HIDDEN, List(XML.Text(txt)))
wenzelm@34002
    49
wenzelm@34002
    50
  def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
wenzelm@34002
    51
  def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
wenzelm@34002
    52
wenzelm@33984
    53
  def spans(tree: XML.Tree): List[XML.Tree] =
wenzelm@33984
    54
    tree match {
wenzelm@38230
    55
      case XML.Elem(Markup(name, _), ts) =>
wenzelm@34046
    56
        List(XML.elem(Markup.DATA, List(tree, span(name, ts.flatMap(spans)))))
wenzelm@34000
    57
      case XML.Text(txt) =>
wenzelm@34000
    58
        val ts = new ListBuffer[XML.Tree]
wenzelm@34000
    59
        val t = new StringBuilder
wenzelm@34002
    60
        def flush() {
wenzelm@34000
    61
          if (!t.isEmpty) {
wenzelm@36012
    62
            ts += XML.Text(t.toString)
wenzelm@34000
    63
            t.clear
wenzelm@34000
    64
          }
wenzelm@33984
    65
        }
wenzelm@34002
    66
        def add(elem: XML.Tree) {
wenzelm@34002
    67
          flush()
wenzelm@36012
    68
          ts += elem
wenzelm@34002
    69
        }
wenzelm@36011
    70
        val syms = Symbol.iterator(txt).map(_.toString)
wenzelm@34002
    71
        while (syms.hasNext) {
wenzelm@34002
    72
          val s1 = syms.next
wenzelm@34006
    73
          def s2() = if (syms.hasNext) syms.next else ""
wenzelm@34002
    74
          s1 match {
wenzelm@34002
    75
            case "\n" => add(XML.elem(BR))
wenzelm@36016
    76
            case "\\<^bsub>" => t ++= s1  // FIXME
wenzelm@36016
    77
            case "\\<^esub>" => t ++= s1  // FIXME
wenzelm@36016
    78
            case "\\<^bsup>" => t ++= s1  // FIXME
wenzelm@36016
    79
            case "\\<^esup>" => t ++= s1  // FIXME
wenzelm@34006
    80
            case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
wenzelm@34006
    81
            case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
wenzelm@34006
    82
            case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
wenzelm@34006
    83
            case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
wenzelm@36016
    84
            case _ => t ++= s1
wenzelm@34000
    85
          }
wenzelm@34000
    86
        }
wenzelm@34002
    87
        flush()
wenzelm@34000
    88
        ts.toList
wenzelm@33984
    89
    }
wenzelm@33984
    90
}