src/Pure/Thy/html.scala
author wenzelm
Sun, 21 May 2017 22:57:46 +0200
changeset 65892 bbad8162d678
parent 65891 586911118317
child 65939 9fb044904a4d
permissions -rw-r--r--
clarified signature;
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
62104
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 60215
diff changeset
    14
  val control =
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 60215
diff changeset
    15
    Map(
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 60215
diff changeset
    16
      Symbol.sub -> "sub",
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 60215
diff changeset
    17
      Symbol.sub_decoded -> "sub",
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 60215
diff changeset
    18
      Symbol.sup -> "sup",
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    19
      Symbol.sup_decoded -> "sup",
62104
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 60215
diff changeset
    20
      Symbol.bold -> "b",
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    21
      Symbol.bold_decoded -> "b")
37200
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    22
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    23
  def output(text: String, s: StringBuilder)
37200
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    24
  {
62113
16de2a9b5b3d tuned -- according to ML version;
wenzelm
parents: 62104
diff changeset
    25
    def output_char(c: Char) =
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    26
      c match {
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    27
        case '<' => s ++= "&lt;"
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    28
        case '>' => s ++= "&gt;"
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    29
        case '&' => s ++= "&amp;"
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    30
        case '"' => s ++= "&quot;"
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    31
        case '\'' => s ++= "&#39;"
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    32
        case '\n' => s ++= "<br/>"
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    33
        case _ => s += c
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    34
      }
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    35
    def output_chars(str: String) = str.iterator.foreach(output_char(_))
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    36
62104
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 60215
diff changeset
    37
    var ctrl = ""
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    38
    for (sym <- Symbol.iterator(text)) {
62104
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 60215
diff changeset
    39
      if (control.isDefinedAt(sym)) ctrl = sym
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    40
      else {
62104
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 60215
diff changeset
    41
        control.get(ctrl) match {
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    42
          case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    43
            s ++= ("<" + elem + ">")
62113
16de2a9b5b3d tuned -- according to ML version;
wenzelm
parents: 62104
diff changeset
    44
            output_chars(sym)
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    45
            s ++= ("</" + elem + ">")
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    46
          case _ =>
62113
16de2a9b5b3d tuned -- according to ML version;
wenzelm
parents: 62104
diff changeset
    47
            output_chars(ctrl)
16de2a9b5b3d tuned -- according to ML version;
wenzelm
parents: 62104
diff changeset
    48
            output_chars(sym)
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    49
        }
62104
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 60215
diff changeset
    50
        ctrl = ""
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    51
      }
37200
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    52
    }
62113
16de2a9b5b3d tuned -- according to ML version;
wenzelm
parents: 62104
diff changeset
    53
    output_chars(ctrl)
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    54
  }
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    55
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    56
  def output(text: String): String = Library.make_string(output(text, _))
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    57
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    58
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    59
  /* output XML as HTML */
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    60
65834
67a6e0f166c2 extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents: 65773
diff changeset
    61
  private val structural_elements =
67a6e0f166c2 extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents: 65773
diff changeset
    62
    Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6",
67a6e0f166c2 extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents: 65773
diff changeset
    63
      "ul", "ol", "dl", "li", "dt", "dd")
67a6e0f166c2 extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents: 65773
diff changeset
    64
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    65
  def output(body: XML.Body, s: StringBuilder)
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    66
  {
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    67
    def attrib(p: (String, String)): Unit =
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    68
      { s ++= " "; s ++= p._1; s ++= "=\""; output(p._2, s); s ++= "\"" }
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    69
    def elem(markup: Markup): Unit =
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    70
      { s ++= markup.name; markup.properties.foreach(attrib) }
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    71
    def tree(t: XML.Tree): Unit =
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    72
      t match {
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    73
        case XML.Elem(markup, Nil) =>
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    74
          s ++= "<"; elem(markup); s ++= "/>"
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    75
        case XML.Elem(markup, ts) =>
65834
67a6e0f166c2 extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents: 65773
diff changeset
    76
          if (structural_elements(markup.name)) s += '\n'
67a6e0f166c2 extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents: 65773
diff changeset
    77
          s ++= "<"; elem(markup); s ++= ">"
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    78
          ts.foreach(tree)
65834
67a6e0f166c2 extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents: 65773
diff changeset
    79
          s ++= "</"; s ++= markup.name; s ++= ">"
67a6e0f166c2 extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents: 65773
diff changeset
    80
          if (structural_elements(markup.name)) s += '\n'
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    81
        case XML.Text(txt) => output(txt, s)
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    82
      }
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    83
    body.foreach(tree)
37200
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    84
  }
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    85
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    86
  def output(body: XML.Body): String = Library.make_string(output(body, _))
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    87
  def output(tree: XML.Tree): String = output(List(tree))
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    88
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    89
65753
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
    90
  /* attributes */
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
    91
65773
120ef768c84c clarified image size;
wenzelm
parents: 65771
diff changeset
    92
  def id(s: String): XML.Attribute = ("id" -> s)
120ef768c84c clarified image size;
wenzelm
parents: 65771
diff changeset
    93
  def width(w: Int): XML.Attribute = ("width" -> w.toString)
120ef768c84c clarified image size;
wenzelm
parents: 65771
diff changeset
    94
  def height(h: Int): XML.Attribute = ("height" -> h.toString)
65892
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
    95
  def css_class(name: String): XML.Attribute = ("class" -> name)
65753
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
    96
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
    97
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
    98
  /* structured markup operators */
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
    99
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   100
  def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
65753
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
   101
  val break: XML.Body = List(XML.elem("br"))
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   102
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   103
  class Operator(name: String)
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   104
  { def apply(body: XML.Body): XML.Elem = XML.elem(name, body) }
64356
wenzelm
parents: 64355
diff changeset
   105
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   106
  class Heading(name: String) extends Operator(name)
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   107
  { def apply(txt: String): XML.Elem = super.apply(text(txt)) }
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   108
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   109
  val div = new Operator("div")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   110
  val span = new Operator("span")
65753
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
   111
  val pre = new Operator("pre")
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   112
  val par = new Operator("p")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   113
  val emph = new Operator("em")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   114
  val bold = new Operator("b")
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65753
diff changeset
   115
  val code = new Operator("code")
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
   116
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   117
  val title = new Heading("title")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   118
  val chapter = new Heading("h1")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   119
  val section = new Heading("h2")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   120
  val subsection = new Heading("h3")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   121
  val subsubsection = new Heading("h4")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   122
  val paragraph = new Heading("h5")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   123
  val subparagraph = new Heading("h6")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   124
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   125
  def itemize(items: List[XML.Body]): XML.Elem =
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   126
    XML.elem("ul", items.map(XML.elem("li", _)))
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   127
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   128
  def enumerate(items: List[XML.Body]): XML.Elem =
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   129
    XML.elem("ol", items.map(XML.elem("li", _)))
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   130
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   131
  def description(items: List[(XML.Body, XML.Body)]): XML.Elem =
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   132
    XML.elem("dl", items.flatMap({ case (x, y) => List(XML.elem("dt", x), XML.elem("dd", y)) }))
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   133
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   134
  def link(href: String, body: XML.Body = Nil): XML.Elem =
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   135
    XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body)
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
   136
65753
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
   137
  def image(src: String, alt: String = ""): XML.Elem =
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
   138
    XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
   139
37200
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
   140
65892
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   141
  /* messages */
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   142
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   143
  val writeln_message_class: XML.Attribute = css_class("writeln_message")
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   144
  val warning_message_class: XML.Attribute = css_class("warning_message")
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   145
  val error_message_class: XML.Attribute = css_class("error_message")
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   146
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   147
  def writeln_message(msg: String): XML.Elem = par(text(msg)) + writeln_message_class
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   148
  def warning_message(msg: String): XML.Elem = par(text(msg)) + warning_message_class
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   149
  def error_message(msg: String): XML.Elem = par(text(msg)) + error_message_class
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   150
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   151
  def writeln_message_span(msg: String): XML.Elem = span(text(msg)) + writeln_message_class
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   152
  def warning_message_span(msg: String): XML.Elem = span(text(msg)) + warning_message_class
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   153
  def error_message_span(msg: String): XML.Elem = span(text(msg)) + error_message_class
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   154
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   155
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   156
  /* document */
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   157
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   158
  val header: String =
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   159
    """<?xml version="1.0" encoding="utf-8" ?>
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   160
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   161
<html xmlns="http://www.w3.org/1999/xhtml">"""
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   162
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   163
  val head_meta: XML.Elem =
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   164
    XML.Elem(Markup("meta",
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   165
      List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil)
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   166
65836
3b4877fbd9cb more systematic HTML.init_dir with css;
wenzelm
parents: 65834
diff changeset
   167
  def head_css(css: String): XML.Elem =
3b4877fbd9cb more systematic HTML.init_dir with css;
wenzelm
parents: 65834
diff changeset
   168
    XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> css)), Nil)
3b4877fbd9cb more systematic HTML.init_dir with css;
wenzelm
parents: 65834
diff changeset
   169
3b4877fbd9cb more systematic HTML.init_dir with css;
wenzelm
parents: 65834
diff changeset
   170
  def output_document(head: XML.Body, body: XML.Body, css: String = "isabelle.css"): String =
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   171
    cat_lines(
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   172
      List(header,
65836
3b4877fbd9cb more systematic HTML.init_dir with css;
wenzelm
parents: 65834
diff changeset
   173
        output(XML.elem("head", head_meta :: (if (css == "") Nil else List(head_css(css))) ::: head)),
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   174
        output(XML.elem("body", body))))
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   175
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   176
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   177
  /* document directory */
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   178
65836
3b4877fbd9cb more systematic HTML.init_dir with css;
wenzelm
parents: 65834
diff changeset
   179
  def init_dir(dir: Path)
3b4877fbd9cb more systematic HTML.init_dir with css;
wenzelm
parents: 65834
diff changeset
   180
  {
3b4877fbd9cb more systematic HTML.init_dir with css;
wenzelm
parents: 65834
diff changeset
   181
    Isabelle_System.mkdirs(dir)
3b4877fbd9cb more systematic HTML.init_dir with css;
wenzelm
parents: 65834
diff changeset
   182
    File.copy(Path.explode("~~/etc/isabelle.css"), dir)
3b4877fbd9cb more systematic HTML.init_dir with css;
wenzelm
parents: 65834
diff changeset
   183
  }
3b4877fbd9cb more systematic HTML.init_dir with css;
wenzelm
parents: 65834
diff changeset
   184
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   185
  def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   186
    css: String = "isabelle.css")
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   187
  {
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   188
    init_dir(dir)
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   189
    File.write(dir + Path.basic(name), output_document(head, body, css))
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   190
  }
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   191
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   192
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   193
  /* Isabelle document */
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   194
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   195
  def begin_document(title: String): String =
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   196
    header + "\n" +
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   197
    "<head>\n" + output(head_meta) + "\n" +
62113
16de2a9b5b3d tuned -- according to ML version;
wenzelm
parents: 62104
diff changeset
   198
    "<title>" + output(title + " (" + Distribution.version + ")") + "</title>\n" +
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   199
    "<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
   200
    "</head>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   201
    "\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   202
    "<body>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   203
    "<div class=\"head\">" +
62113
16de2a9b5b3d tuned -- according to ML version;
wenzelm
parents: 62104
diff changeset
   204
    "<h1>" + output(title) + "</h1>\n"
16de2a9b5b3d tuned -- according to ML version;
wenzelm
parents: 62104
diff changeset
   205
16de2a9b5b3d tuned -- according to ML version;
wenzelm
parents: 62104
diff changeset
   206
  val end_document = "\n</div>\n</body>\n</html>\n"
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   207
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   208
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   209
  /* common markup elements */
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
   210
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
   211
  private def session_entry(entry: (String, String)): String =
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
   212
  {
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
   213
    val (name, description) = entry
65753
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
   214
    val descr = if (description == "") Nil else break ::: List(pre(text(description)))
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents: 50201
diff changeset
   215
    XML.string_of_tree(
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents: 50201
diff changeset
   216
      XML.elem("li",
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents: 50201
diff changeset
   217
        List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
   218
          List(XML.Text(name)))) ::: descr)) + "\n"
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
   219
  }
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
   220
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
   221
  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
   222
  {
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   223
    begin_document("Isabelle/" + chapter + " sessions") +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   224
      (if (sessions.isEmpty) ""
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   225
       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
   226
    end_document
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   227
  }
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
   228
}