src/Pure/Thy/html.scala
author wenzelm
Sun, 22 Aug 2010 13:52:24 +0200
changeset 38573 d163f0f28e8c
parent 38444 796904799f4d
child 43455 4b4b93672f15
permissions -rw-r--r--
tuned signatures;
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
38573
d163f0f28e8c tuned signatures;
wenzelm
parents: 38444
diff changeset
    44
  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
    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
38573
d163f0f28e8c tuned signatures;
wenzelm
parents: 38444
diff changeset
    53
  def spans(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
    54
  {
38573
d163f0f28e8c tuned signatures;
wenzelm
parents: 38444
diff changeset
    55
    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
    56
      tree match {
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
    57
        case XML.Elem(Markup(name, _), ts) =>
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
    58
          if (original_data)
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
    59
            List(XML.Elem(Markup.Data, List(tree, span(name, ts.flatMap(html_spans)))))
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
          else List(span(name, ts.flatMap(html_spans)))
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
    61
        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
    62
          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
    63
          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
    64
          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
    65
            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
    66
              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
    67
              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
    68
            }
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    69
          }
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
    70
          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
    71
            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
    72
            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
    73
          }
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
          val syms = Symbol.iterator(txt).map(_.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
          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
    76
            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
    77
            def s2() = if (syms.hasNext) syms.next else ""
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
            s1 match {
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
              case "\n" => add(XML.elem(BR))
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
              case "\\<^bsub>" => t ++= s1  // FIXME
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
              case "\\<^esub>" => t ++= s1  // FIXME
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
    82
              case "\\<^bsup>" => t ++= s1  // FIXME
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
              case "\\<^esup>" => t ++= s1  // FIXME
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
              case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
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
              case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
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
    86
              case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
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
    87
              case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
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
    88
              case _ => t ++= s1
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
    89
            }
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
    90
          }
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    91
          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
    92
          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
    93
      }
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
    94
    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
    95
  }
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    96
}