src/Pure/Thy/html.scala
author wenzelm
Sat, 25 Jun 2011 18:15:36 +0200
changeset 43548 f231a7594e54
parent 43511 d138e7482a1b
child 43661 39fdbd814c7f
permissions -rw-r--r--
type classes: entity markup instead of old-style token 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"
43490
5e6f76cacb93 more uniform treatment of recode_set/recode_map;
wenzelm
parents: 43489
diff changeset
    40
  val STYLE = "style"
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    41
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    42
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    43
  // document markup
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    44
38573
d163f0f28e8c tuned signatures;
wenzelm
parents: 38444
diff changeset
    45
  def span(cls: String, body: XML.Body): XML.Elem =
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 37200
diff changeset
    46
    XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    47
43490
5e6f76cacb93 more uniform treatment of recode_set/recode_map;
wenzelm
parents: 43489
diff changeset
    48
  def user_font(font: String, txt: String): XML.Elem =
5e6f76cacb93 more uniform treatment of recode_set/recode_map;
wenzelm
parents: 43489
diff changeset
    49
    XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))
5e6f76cacb93 more uniform treatment of recode_set/recode_map;
wenzelm
parents: 43489
diff changeset
    50
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    51
  def hidden(txt: String): XML.Elem =
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    52
    span(Markup.HIDDEN, List(XML.Text(txt)))
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    53
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    54
  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
    55
  def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
43459
wenzelm
parents: 43458
diff changeset
    56
  def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt)))
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    57
43455
4b4b93672f15 some unicode chars for special control symbols;
wenzelm
parents: 38573
diff changeset
    58
  def spans(symbols: Symbol.Interpretation,
4b4b93672f15 some unicode chars for special control symbols;
wenzelm
parents: 38573
diff changeset
    59
    input: XML.Tree, original_data: Boolean = false): XML.Body =
38444
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    60
  {
38573
d163f0f28e8c tuned signatures;
wenzelm
parents: 38444
diff changeset
    61
    def html_spans(tree: XML.Tree): XML.Body =
38444
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    62
      tree match {
43548
f231a7594e54 type classes: entity markup instead of old-style token markup;
wenzelm
parents: 43511
diff changeset
    63
        case XML.Elem(m @ Markup(name, props), ts) =>
f231a7594e54 type classes: entity markup instead of old-style token markup;
wenzelm
parents: 43511
diff changeset
    64
          val span_class =
f231a7594e54 type classes: entity markup instead of old-style token markup;
wenzelm
parents: 43511
diff changeset
    65
            m match { case Markup.Entity(kind, _) => name + "_" + kind case _ => name }
f231a7594e54 type classes: entity markup instead of old-style token markup;
wenzelm
parents: 43511
diff changeset
    66
          val html_span = span(span_class, ts.flatMap(html_spans))
f231a7594e54 type classes: entity markup instead of old-style token markup;
wenzelm
parents: 43511
diff changeset
    67
          if (original_data) List(XML.Elem(Markup.Data, List(tree, html_span)))
f231a7594e54 type classes: entity markup instead of old-style token markup;
wenzelm
parents: 43511
diff changeset
    68
          else List(html_span)
38444
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    69
        case XML.Text(txt) =>
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    70
          val ts = new ListBuffer[XML.Tree]
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    71
          val t = new StringBuilder
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    72
          def flush() {
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    73
            if (!t.isEmpty) {
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    74
              ts += XML.Text(t.toString)
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    75
              t.clear
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    76
            }
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    77
          }
38444
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    78
          def add(elem: XML.Tree) {
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    79
            flush()
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    80
            ts += elem
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    81
          }
43489
132f99cc0a43 tuned iteration over short symbols;
wenzelm
parents: 43459
diff changeset
    82
          val syms = Symbol.iterator_string(txt)
38444
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    83
          while (syms.hasNext) {
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    84
            val s1 = syms.next
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    85
            def s2() = if (syms.hasNext) syms.next else ""
43455
4b4b93672f15 some unicode chars for special control symbols;
wenzelm
parents: 38573
diff changeset
    86
            if (s1 == "\n") add(XML.elem(BR))
43511
d138e7482a1b clarified decoded control symbols;
wenzelm
parents: 43490
diff changeset
    87
            else if (s1 == symbols.bsub_decoded) t ++= s1  // FIXME
d138e7482a1b clarified decoded control symbols;
wenzelm
parents: 43490
diff changeset
    88
            else if (s1 == symbols.esub_decoded) t ++= s1  // FIXME
d138e7482a1b clarified decoded control symbols;
wenzelm
parents: 43490
diff changeset
    89
            else if (s1 == symbols.bsup_decoded) t ++= s1  // FIXME
d138e7482a1b clarified decoded control symbols;
wenzelm
parents: 43490
diff changeset
    90
            else if (s1 == symbols.esup_decoded) t ++= s1  // FIXME
43459
wenzelm
parents: 43458
diff changeset
    91
            else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
wenzelm
parents: 43458
diff changeset
    92
            else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
43511
d138e7482a1b clarified decoded control symbols;
wenzelm
parents: 43490
diff changeset
    93
            else if (s1 == symbols.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
43490
5e6f76cacb93 more uniform treatment of recode_set/recode_map;
wenzelm
parents: 43489
diff changeset
    94
            else if (symbols.fonts.isDefinedAt(s1)) { add(user_font(symbols.fonts(s1), s1)) }
43455
4b4b93672f15 some unicode chars for special control symbols;
wenzelm
parents: 38573
diff changeset
    95
            else t ++= s1
38444
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    96
          }
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    97
          flush()
38444
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    98
          ts.toList
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
    99
      }
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
   100
    html_spans(input)
796904799f4d HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents: 38231
diff changeset
   101
  }
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
   102
}