src/Pure/Thy/html.scala
author wenzelm
Sun, 12 Apr 2015 13:10:04 +0200
changeset 60033 9a1d40876e9f
parent 59063 b3c45d0e4fe1
child 60215 5fb4990dfc73
permissions -rw-r--r--
less ambitious collection of quasi-generic PIDE modules;
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
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents: 50201
diff changeset
     4
HTML presentation elements.
33984
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
55618
995162143ef4 tuned imports;
wenzelm
parents: 54379
diff changeset
     9
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    10
object HTML
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    11
{
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    12
  /* encode text with control symbols */
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    13
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    14
  val control_decoded =
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    15
    Map(Symbol.sub_decoded -> "sub",
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    16
      Symbol.sup_decoded -> "sup",
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    17
      Symbol.bold_decoded -> "b")
37200
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    18
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    19
  def encode(text: String): String =
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    20
  {
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    21
    val result = new StringBuilder
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    22
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    23
    def encode_char(c: Char) =
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    24
      c match {
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    25
        case '<' => result ++= "&lt;"
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    26
        case '>' => result ++= "&gt;"
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    27
        case '&' => result ++= "&amp;"
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    28
        case '"' => result ++= "&quot;"
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    29
        case '\'' => result ++= "&#39;"
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    30
        case '\n' => result ++= "<br/>"
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    31
        case c => result += c
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    32
      }
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    33
    def encode_chars(s: String) = s.iterator.foreach(encode_char(_))
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    34
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    35
    var control = ""
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    36
    for (sym <- Symbol.iterator(text)) {
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    37
      if (control_decoded.isDefinedAt(sym)) control = sym
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    38
      else {
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    39
        control_decoded.get(control) match {
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    40
          case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    41
            result ++= ("<" + elem + ">")
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    42
            encode_chars(sym)
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    43
            result ++= ("</" + elem + ">")
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    44
          case _ =>
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    45
            encode_chars(control)
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    46
            encode_chars(sym)
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    47
        }
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    48
        control = ""
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    49
      }
37200
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    50
    }
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    51
    encode_chars(control)
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    52
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    53
    result.toString
37200
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    54
  }
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    55
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    56
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    57
  /* document */
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    58
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    59
  val end_document = "\n</div>\n</body>\n</html>\n"
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    60
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    61
  def begin_document(title: String): String =
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    62
    "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    63
    "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    64
    "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    65
    "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    66
    "<head>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    67
    "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    68
    "<title>" + encode(title) + "</title>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    69
    "<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    70
    "</head>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    71
    "\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    72
    "<body>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    73
    "<div class=\"head\">" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    74
    "<h1>" + encode(title) + "</h1>\n"
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    75
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    76
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    77
  /* common markup elements */
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    78
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    79
  private def session_entry(entry: (String, String)): String =
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    80
  {
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    81
    val (name, description) = entry
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    82
    val descr =
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    83
      if (description == "") Nil
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    84
      else List(XML.elem("br"), XML.elem("pre", List(XML.Text(description))))
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents: 50201
diff changeset
    85
    XML.string_of_tree(
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents: 50201
diff changeset
    86
      XML.elem("li",
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents: 50201
diff changeset
    87
        List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    88
          List(XML.Text(name)))) ::: descr)) + "\n"
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    89
  }
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    90
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    91
  def chapter_index(chapter: String, sessions: List[(String, String)]): String =
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    92
  {
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    93
    begin_document("Isabelle/" + chapter + " sessions") +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    94
      (if (sessions.isEmpty) ""
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    95
       else "<div class=\"sessions\"><ul>\n" + sessions.map(session_entry(_)).mkString + "</ul>") +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    96
    end_document
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    97
  }
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    98
}