src/Pure/Thy/html.scala
author wenzelm
Sat, 07 Aug 2010 22:43:57 +0200
changeset 38231 968844caaff9
parent 38230 ed147003de4b
child 38444 796904799f4d
permissions -rw-r--r--
simplified some Markup;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Thy/html.scala
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
     3
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
     4
Basic HTML output.
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
     5
*/
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
     6
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
     7
package isabelle
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
     8
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
     9
import scala.collection.mutable.ListBuffer
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    10
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    11
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    12
object HTML
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    13
{
37200
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    14
  // encode text
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    15
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    16
  def encode(text: String): String =
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    17
  {
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    18
    val s = new StringBuilder
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    19
    for (c <- text.iterator) c match {
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    20
      case '<' => s ++= "&lt;"
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    21
      case '>' => s ++= "&gt;"
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    22
      case '&' => s ++= "&amp;"
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    23
      case '"' => s ++= "&quot;"
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    24
      case '\'' => s ++= "&#39;"
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    25
      case '\n' => s ++= "<br/>"
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    26
      case _ => s += c
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    27
    }
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    28
    s.toString
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    29
  }
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    30
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    31
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    32
  // common elements and attributes
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    33
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    34
  val BODY = "body"
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    35
  val DIV = "div"
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    36
  val SPAN = "span"
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    37
  val BR = "br"
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    38
  val PRE = "pre"
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    39
  val CLASS = "class"
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    40
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    41
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    42
  // document markup
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    43
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    44
  def span(cls: String, body: List[XML.Tree]): XML.Elem =
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 37200
diff changeset
    45
    XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    46
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    47
  def hidden(txt: String): XML.Elem =
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    48
    span(Markup.HIDDEN, List(XML.Text(txt)))
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    49
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    50
  def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    51
  def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    52
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    53
  def spans(tree: XML.Tree): List[XML.Tree] =
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    54
    tree match {
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 37200
diff changeset
    55
      case XML.Elem(Markup(name, _), ts) =>
38231
968844caaff9 simplified some Markup;
wenzelm
parents: 38230
diff changeset
    56
        List(XML.Elem(Markup.Data, List(tree, span(name, ts.flatMap(spans)))))
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    57
      case XML.Text(txt) =>
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    58
        val ts = new ListBuffer[XML.Tree]
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    59
        val t = new StringBuilder
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    60
        def flush() {
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    61
          if (!t.isEmpty) {
36012
0614676f14d4 replaced some deprecated methods;
wenzelm
parents: 36011
diff changeset
    62
            ts += XML.Text(t.toString)
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    63
            t.clear
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    64
          }
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    65
        }
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    66
        def add(elem: XML.Tree) {
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    67
          flush()
36012
0614676f14d4 replaced some deprecated methods;
wenzelm
parents: 36011
diff changeset
    68
          ts += elem
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    69
        }
36011
3ff725ac13a4 adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents: 34137
diff changeset
    70
        val syms = Symbol.iterator(txt).map(_.toString)
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    71
        while (syms.hasNext) {
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    72
          val s1 = syms.next
34006
bbd146caa6b2 avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents: 34004
diff changeset
    73
          def s2() = if (syms.hasNext) syms.next else ""
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    74
          s1 match {
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    75
            case "\n" => add(XML.elem(BR))
36016
4f5c7a19ebe0 recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents: 36012
diff changeset
    76
            case "\\<^bsub>" => t ++= s1  // FIXME
4f5c7a19ebe0 recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents: 36012
diff changeset
    77
            case "\\<^esub>" => t ++= s1  // FIXME
4f5c7a19ebe0 recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents: 36012
diff changeset
    78
            case "\\<^bsup>" => t ++= s1  // FIXME
4f5c7a19ebe0 recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents: 36012
diff changeset
    79
            case "\\<^esup>" => t ++= s1  // FIXME
34006
bbd146caa6b2 avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents: 34004
diff changeset
    80
            case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
bbd146caa6b2 avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents: 34004
diff changeset
    81
            case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
bbd146caa6b2 avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents: 34004
diff changeset
    82
            case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
bbd146caa6b2 avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents: 34004
diff changeset
    83
            case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
36016
4f5c7a19ebe0 recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents: 36012
diff changeset
    84
            case _ => t ++= s1
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    85
          }
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    86
        }
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    87
        flush()
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    88
        ts.toList
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    89
    }
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    90
}