src/Pure/Thy/html.scala
author wenzelm
Sat, 24 Nov 2018 18:56:44 +0100
changeset 69343 395c4fb15ea2
parent 67337 4254cfd15b00
child 69355 cdc2de88d657
permissions -rw-r--r--
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
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
{
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    12
  /* output text with control symbols */
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    13
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    14
  private val control =
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    15
    Map(
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    16
      Symbol.sub -> "sub", Symbol.sub_decoded -> "sub",
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    17
      Symbol.sup -> "sup", Symbol.sup_decoded -> "sup",
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    18
      Symbol.bold -> "b", Symbol.bold_decoded -> "b")
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    19
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    20
  private val control_block =
62104
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 60215
diff changeset
    21
    Map(
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    22
      Symbol.bsub -> "<sub>", Symbol.bsub_decoded -> "<sub>",
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    23
      Symbol.esub -> "</sub>", Symbol.esub_decoded -> "</sub>",
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    24
      Symbol.bsup -> "<sup>", Symbol.bsup_decoded -> "<sup>",
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    25
      Symbol.esup -> "</sup>", Symbol.esup_decoded -> "</sup>")
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    26
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    27
  def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym)
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    28
66018
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    29
  def output_char_permissive(c: Char, s: StringBuilder)
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    30
  {
66018
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    31
    c match {
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    32
      case '<' => s ++= "&lt;"
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    33
      case '>' => s ++= "&gt;"
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    34
      case '&' => s ++= "&amp;"
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    35
      case _ => s += c
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    36
    }
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    37
  }
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    38
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    39
  def output(text: String, s: StringBuilder, hidden: Boolean, permissive: Boolean)
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    40
  {
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    41
    def output_char(c: Char): Unit =
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    42
      if (permissive) output_char_permissive(c, s)
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    43
      else XML.output_char(c, s)
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    44
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    45
    def output_string(str: String): Unit =
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    46
      str.iterator.foreach(output_char)
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    47
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    48
    def output_hidden(body: => Unit): Unit =
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    49
      if (hidden) { s ++= "<span class=\"hidden\">"; body; s ++= "</span>" }
37200
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    50
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    51
    def output_symbol(sym: Symbol.Symbol): Unit =
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    52
      if (sym != "") {
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    53
        control_block.get(sym) match {
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    54
          case Some(html) if html.startsWith("</") =>
66018
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    55
            s ++= html; output_hidden(output_string(sym))
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    56
          case Some(html) =>
66018
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    57
            output_hidden(output_string(sym)); s ++= html
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    58
          case None =>
67255
f1f983484878 HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents: 66212
diff changeset
    59
            if (hidden && Symbol.is_control_encoded(sym)) {
f1f983484878 HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents: 66212
diff changeset
    60
              output_hidden(output_string(Symbol.control_prefix))
f1f983484878 HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents: 66212
diff changeset
    61
              s ++= "<span class=\"control\">"
f1f983484878 HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents: 66212
diff changeset
    62
              output_string(Symbol.control_name(sym).get)
f1f983484878 HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents: 66212
diff changeset
    63
              s ++= "</span>"
f1f983484878 HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents: 66212
diff changeset
    64
              output_hidden(output_string(Symbol.control_suffix))
f1f983484878 HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents: 66212
diff changeset
    65
            }
f1f983484878 HTML rendering of \<^control> as in Isabelle/jEdit;
wenzelm
parents: 66212
diff changeset
    66
            else output_string(sym)
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    67
        }
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    68
      }
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    69
62104
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 60215
diff changeset
    70
    var ctrl = ""
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    71
    for (sym <- Symbol.iterator(text)) {
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    72
      if (is_control(sym)) { output_symbol(ctrl); ctrl = sym }
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    73
      else {
62104
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 60215
diff changeset
    74
        control.get(ctrl) match {
66006
cec184536dfd uniform notion of Symbol.is_controllable (see also 265d9300d523);
wenzelm
parents: 66001
diff changeset
    75
          case Some(elem) if Symbol.is_controllable(sym) =>
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    76
            output_hidden(output_symbol(ctrl))
65991
wenzelm
parents: 65990
diff changeset
    77
            s += '<'; s ++= elem; s += '>'
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    78
            output_symbol(sym)
65991
wenzelm
parents: 65990
diff changeset
    79
            s ++= "</"; s ++= elem; s += '>'
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    80
          case _ =>
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    81
            output_symbol(ctrl)
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    82
            output_symbol(sym)
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    83
        }
62104
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 60215
diff changeset
    84
        ctrl = ""
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    85
      }
37200
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
    86
    }
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
    87
    output_symbol(ctrl)
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    88
  }
59063
b3c45d0e4fe1 encode text with control symbols;
wenzelm
parents: 56748
diff changeset
    89
66018
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    90
  def output(text: String): String =
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
    91
    Library.make_string(output(text, _, hidden = false, permissive = true))
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    92
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    93
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    94
  /* output XML as HTML */
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
    95
65834
67a6e0f166c2 extra space only for some structual elements, but not <a>, <b>, <em> etc. (amending 8a0fe5469ba0);
wenzelm
parents: 65773
diff changeset
    96
  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
    97
    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
    98
      "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
    99
67337
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   100
  def output(body: XML.Body, s: StringBuilder, hidden: Boolean, structural: Boolean)
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
   101
  {
65991
wenzelm
parents: 65990
diff changeset
   102
    def elem(markup: Markup)
wenzelm
parents: 65990
diff changeset
   103
    {
wenzelm
parents: 65990
diff changeset
   104
      s ++= markup.name
wenzelm
parents: 65990
diff changeset
   105
      for ((a, b) <- markup.properties) {
66018
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
   106
        s += ' '
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
   107
        s ++= a
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
   108
        s += '='
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
   109
        s += '"'
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
   110
        output(b, s, hidden = hidden, permissive = false)
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
   111
        s += '"'
65991
wenzelm
parents: 65990
diff changeset
   112
      }
wenzelm
parents: 65990
diff changeset
   113
    }
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
   114
    def tree(t: XML.Tree): Unit =
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
   115
      t match {
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
   116
        case XML.Elem(markup, Nil) =>
65991
wenzelm
parents: 65990
diff changeset
   117
          s += '<'; elem(markup); s ++= "/>"
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
   118
        case XML.Elem(markup, ts) =>
67337
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   119
          if (structural && structural_elements(markup.name)) s += '\n'
65991
wenzelm
parents: 65990
diff changeset
   120
          s += '<'; elem(markup); s += '>'
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
   121
          ts.foreach(tree)
65991
wenzelm
parents: 65990
diff changeset
   122
          s ++= "</"; s ++= markup.name; s += '>'
67337
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   123
          if (structural && structural_elements(markup.name)) s += '\n'
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
   124
        case XML.Text(txt) =>
66018
9ce3720976dc permissive output of XML.Text, e.g. relevant for embedded <style>;
wenzelm
parents: 66006
diff changeset
   125
          output(txt, s, hidden = hidden, permissive = true)
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
   126
      }
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
   127
    body.foreach(tree)
37200
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
   128
  }
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
   129
67337
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   130
  def output(body: XML.Body, hidden: Boolean, structural: Boolean): String =
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   131
    Library.make_string(output(body, _, hidden, structural))
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
   132
67337
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   133
  def output(tree: XML.Tree, hidden: Boolean, structural: Boolean): String =
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   134
    output(List(tree), hidden, structural)
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
   135
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
   136
65753
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
   137
  /* attributes */
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
   138
65992
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   139
  class Attribute(val name: String, value: String)
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   140
  {
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   141
    def xml: XML.Attribute = name -> value
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   142
    def apply(elem: XML.Elem): XML.Elem = elem + xml
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   143
  }
65942
864a4892e43c clarified signature;
wenzelm
parents: 65941
diff changeset
   144
65992
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   145
  def id(s: String): Attribute = new Attribute("id", s)
65993
75590c9a585f tuned signature;
wenzelm
parents: 65992
diff changeset
   146
  def class_(name: String): Attribute = new Attribute("class", name)
65946
5dd3974cf0bc tuned signature;
wenzelm
parents: 65944
diff changeset
   147
65992
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   148
  def width(w: Int): Attribute = new Attribute("width", w.toString)
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   149
  def height(h: Int): Attribute = new Attribute("height", h.toString)
65946
5dd3974cf0bc tuned signature;
wenzelm
parents: 65944
diff changeset
   150
  def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem))
65753
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
   151
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
   152
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   153
  /* structured markup operators */
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   154
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   155
  def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
67336
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67255
diff changeset
   156
  val no_text: XML.Tree = XML.Text("")
65753
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
   157
  val break: XML.Body = List(XML.elem("br"))
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   158
65992
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   159
  class Operator(val name: String)
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   160
  {
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   161
    def apply(body: XML.Body): XML.Elem = XML.elem(name, body)
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   162
    def apply(att: Attribute, body: XML.Body): XML.Elem = att(apply(body))
65993
75590c9a585f tuned signature;
wenzelm
parents: 65992
diff changeset
   163
    def apply(c: String, body: XML.Body): XML.Elem = apply(class_(c), body)
65992
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   164
  }
64356
wenzelm
parents: 64355
diff changeset
   165
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   166
  class Heading(name: String) extends Operator(name)
65992
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   167
  {
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   168
    def apply(txt: String): XML.Elem = super.apply(text(txt))
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   169
    def apply(att: Attribute, txt: String): XML.Elem = super.apply(att, text(txt))
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   170
    def apply(c: String, txt: String): XML.Elem = super.apply(c, text(txt))
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   171
  }
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   172
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   173
  val div = new Operator("div")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   174
  val span = new Operator("span")
65753
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
   175
  val pre = new Operator("pre")
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   176
  val par = new Operator("p")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   177
  val emph = new Operator("em")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   178
  val bold = new Operator("b")
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65753
diff changeset
   179
  val code = new Operator("code")
67336
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67255
diff changeset
   180
  val item = new Operator("li")
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67255
diff changeset
   181
  val list = new Operator("ul")
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67255
diff changeset
   182
  val enum = new Operator("ol")
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67255
diff changeset
   183
  val descr = new Operator("dl")
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67255
diff changeset
   184
  val dt = new Operator("dt")
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67255
diff changeset
   185
  val dd = new Operator("dd")
64355
c6a1031cf925 support for XML as HTML;
wenzelm
parents: 62113
diff changeset
   186
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   187
  val title = new Heading("title")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   188
  val chapter = new Heading("h1")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   189
  val section = new Heading("h2")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   190
  val subsection = new Heading("h3")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   191
  val subsubsection = new Heading("h4")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   192
  val paragraph = new Heading("h5")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   193
  val subparagraph = new Heading("h6")
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   194
67336
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67255
diff changeset
   195
  def itemize(items: List[XML.Body]): XML.Elem = list(items.map(item(_)))
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67255
diff changeset
   196
  def enumerate(items: List[XML.Body]): XML.Elem = enum(items.map(item(_)))
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   197
  def description(items: List[(XML.Body, XML.Body)]): XML.Elem =
67336
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67255
diff changeset
   198
    descr(items.flatMap({ case (x, y) => List(dt(x), dd(y)) }))
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   199
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   200
  def link(href: String, body: XML.Body = Nil): XML.Elem =
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   201
    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
   202
65753
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
   203
  def image(src: String, alt: String = ""): XML.Elem =
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
   204
    XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
787e5ee6ef53 more operations;
wenzelm
parents: 64362
diff changeset
   205
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66018
diff changeset
   206
  def source(body: XML.Body): XML.Elem = pre("source", body)
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66018
diff changeset
   207
  def source(src: String): XML.Elem = source(text(src))
65988
8040d2563593 modernized generated HTML;
wenzelm
parents: 65946
diff changeset
   208
65941
316c30b60ebc tuned layout;
wenzelm
parents: 65939
diff changeset
   209
  def style(s: String): XML.Elem = XML.elem("style", text(s))
66000
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   210
  def style_file(href: String): XML.Elem =
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   211
    XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)
66212
f41396c15bb1 tuned signature;
wenzelm
parents: 66210
diff changeset
   212
  def style_file(path: Path): XML.Elem = style_file(Url.print_file(path.file))
66000
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   213
66210
a8b936749300 more operations/options;
wenzelm
parents: 66209
diff changeset
   214
  def script(s: String): XML.Elem = XML.elem("script", text(s))
a8b936749300 more operations/options;
wenzelm
parents: 66209
diff changeset
   215
  def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil)
66212
f41396c15bb1 tuned signature;
wenzelm
parents: 66210
diff changeset
   216
  def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file))
f41396c15bb1 tuned signature;
wenzelm
parents: 66210
diff changeset
   217
37200
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents: 36016
diff changeset
   218
65892
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   219
  /* messages */
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   220
65939
9fb044904a4d support for message underline and tooltips;
wenzelm
parents: 65892
diff changeset
   221
  // background
65993
75590c9a585f tuned signature;
wenzelm
parents: 65992
diff changeset
   222
  val writeln_message: Attribute = class_("writeln_message")
75590c9a585f tuned signature;
wenzelm
parents: 65992
diff changeset
   223
  val warning_message: Attribute = class_("warning_message")
75590c9a585f tuned signature;
wenzelm
parents: 65992
diff changeset
   224
  val error_message: Attribute = class_("error_message")
65892
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   225
65939
9fb044904a4d support for message underline and tooltips;
wenzelm
parents: 65892
diff changeset
   226
  // underline
65993
75590c9a585f tuned signature;
wenzelm
parents: 65992
diff changeset
   227
  val writeln: Attribute = class_("writeln")
75590c9a585f tuned signature;
wenzelm
parents: 65992
diff changeset
   228
  val warning: Attribute = class_("warning")
75590c9a585f tuned signature;
wenzelm
parents: 65992
diff changeset
   229
  val error: Attribute = class_("error")
65892
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   230
65944
79e4d94aa9ad tuned signature;
wenzelm
parents: 65943
diff changeset
   231
79e4d94aa9ad tuned signature;
wenzelm
parents: 65943
diff changeset
   232
  /* tooltips */
79e4d94aa9ad tuned signature;
wenzelm
parents: 65943
diff changeset
   233
79e4d94aa9ad tuned signature;
wenzelm
parents: 65943
diff changeset
   234
  def tooltip(item: XML.Body, tip: XML.Body): XML.Elem =
65992
50daca61efd6 tuned signature;
wenzelm
parents: 65991
diff changeset
   235
    span(item ::: List(div("tooltip", tip)))
65944
79e4d94aa9ad tuned signature;
wenzelm
parents: 65943
diff changeset
   236
79e4d94aa9ad tuned signature;
wenzelm
parents: 65943
diff changeset
   237
  def tooltip_errors(item: XML.Body, msgs: List[XML.Body]): XML.Elem =
79e4d94aa9ad tuned signature;
wenzelm
parents: 65943
diff changeset
   238
    HTML.error(tooltip(item, msgs.map(msg => error_message(pre(msg)))))
65892
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   239
bbad8162d678 clarified signature;
wenzelm
parents: 65891
diff changeset
   240
66196
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   241
  /* GUI elements */
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   242
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   243
  object GUI
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   244
  {
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   245
    private def optional_value(text: String): XML.Attributes =
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   246
      proper_string(text).map(a => "value" -> a).toList
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   247
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   248
    private def optional_name(name: String): XML.Attributes =
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   249
      proper_string(name).map(a => "name" -> a).toList
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   250
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   251
    private def optional_title(tooltip: String): XML.Attributes =
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   252
      proper_string(tooltip).map(a => "title" -> a).toList
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   253
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   254
    private def optional_submit(submit: Boolean): XML.Attributes =
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   255
      if (submit) List("onChange" -> "this.form.submit()") else Nil
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   256
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   257
    private def optional_checked(selected: Boolean): XML.Attributes =
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   258
      if (selected) List("checked" -> "") else Nil
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   259
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   260
    private def optional_action(action: String): XML.Attributes =
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   261
      proper_string(action).map(a => "action" -> a).toList
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   262
66210
a8b936749300 more operations/options;
wenzelm
parents: 66209
diff changeset
   263
    private def optional_onclick(script: String): XML.Attributes =
a8b936749300 more operations/options;
wenzelm
parents: 66209
diff changeset
   264
      proper_string(script).map(a => "onclick" -> a).toList
a8b936749300 more operations/options;
wenzelm
parents: 66209
diff changeset
   265
a8b936749300 more operations/options;
wenzelm
parents: 66209
diff changeset
   266
    private def optional_onchange(script: String): XML.Attributes =
a8b936749300 more operations/options;
wenzelm
parents: 66209
diff changeset
   267
      proper_string(script).map(a => "onchange" -> a).toList
a8b936749300 more operations/options;
wenzelm
parents: 66209
diff changeset
   268
a8b936749300 more operations/options;
wenzelm
parents: 66209
diff changeset
   269
    def button(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false,
a8b936749300 more operations/options;
wenzelm
parents: 66209
diff changeset
   270
        script: String = ""): XML.Elem =
66196
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   271
      XML.Elem(
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   272
        Markup("button",
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   273
          List("type" -> (if (submit) "submit" else "button"), "value" -> "true") :::
66210
a8b936749300 more operations/options;
wenzelm
parents: 66209
diff changeset
   274
          optional_name(name) ::: optional_title(tooltip) ::: optional_onclick(script)), body)
66196
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   275
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   276
    def checkbox(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false,
66210
a8b936749300 more operations/options;
wenzelm
parents: 66209
diff changeset
   277
        selected: Boolean = false, script: String = ""): XML.Elem =
66196
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   278
      XML.elem("label",
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   279
        XML.elem(
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   280
          Markup("input",
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   281
            List("type" -> "checkbox", "value" -> "true") ::: optional_name(name) :::
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   282
              optional_title(tooltip) ::: optional_submit(submit) :::
66210
a8b936749300 more operations/options;
wenzelm
parents: 66209
diff changeset
   283
              optional_checked(selected) ::: optional_onchange(script))) :: body)
66196
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   284
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   285
    def text_field(columns: Int = 0, text: String = "", name: String = "", tooltip: String = "",
66210
a8b936749300 more operations/options;
wenzelm
parents: 66209
diff changeset
   286
        submit: Boolean = false, script: String = ""): XML.Elem =
66196
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   287
      XML.elem(Markup("input",
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   288
        List("type" -> "text") :::
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   289
          (if (columns > 0) List("size" -> columns.toString) else Nil) :::
66210
a8b936749300 more operations/options;
wenzelm
parents: 66209
diff changeset
   290
          optional_value(text) ::: optional_name(name) ::: optional_title(tooltip) :::
a8b936749300 more operations/options;
wenzelm
parents: 66209
diff changeset
   291
          optional_submit(submit) ::: optional_onchange(script)))
66196
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   292
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   293
    def parameter(text: String = "", name: String = ""): XML.Elem =
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   294
      XML.elem(
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   295
        Markup("input", List("type" -> "hidden") ::: optional_value(text) ::: optional_name(name)))
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   296
66209
3a4dfe10ab1a clarified signature;
wenzelm
parents: 66206
diff changeset
   297
    def form(body: XML.Body, name: String = "", action: String = "", http_post: Boolean = false)
3a4dfe10ab1a clarified signature;
wenzelm
parents: 66206
diff changeset
   298
        : XML.Elem =
3a4dfe10ab1a clarified signature;
wenzelm
parents: 66206
diff changeset
   299
      XML.Elem(
3a4dfe10ab1a clarified signature;
wenzelm
parents: 66206
diff changeset
   300
        Markup("form", optional_name(name) ::: optional_action(action) :::
3a4dfe10ab1a clarified signature;
wenzelm
parents: 66206
diff changeset
   301
          (if (http_post) List("method" -> "post") else Nil)), body)
66196
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   302
  }
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   303
31c9b09cc1d4 some HTML GUI elements;
wenzelm
parents: 66040
diff changeset
   304
66200
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   305
  /* GUI layout */
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   306
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   307
  object Wrap_Panel
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   308
  {
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   309
    object Alignment extends Enumeration
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   310
    {
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   311
      val left, right, center = Value
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   312
    }
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   313
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   314
    def apply(contents: List[XML.Elem], name: String = "", action: String = "",
66206
2d2082db735a clarified defaults;
wenzelm
parents: 66200
diff changeset
   315
      alignment: Alignment.Value = Alignment.right): XML.Elem =
66200
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   316
    {
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   317
      val body = Library.separate(XML.Text(" "), contents)
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   318
      GUI.form(List(div(body) + ("style" -> ("text-align: " + alignment))),
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   319
        name = name, action = action)
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   320
    }
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   321
  }
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   322
02c66b71c013 GUI layout similar to Pure/GUI/wrap_panel.scala;
wenzelm
parents: 66196
diff changeset
   323
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   324
  /* document */
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   325
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   326
  val header: String =
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   327
    """<?xml version="1.0" encoding="utf-8" ?>
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   328
<!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
   329
<html xmlns="http://www.w3.org/1999/xhtml">"""
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   330
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   331
  val head_meta: XML.Elem =
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   332
    XML.Elem(Markup("meta",
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   333
      List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil)
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   334
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
   335
  def output_document(head: XML.Body, body: XML.Body,
67337
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   336
    css: String = "isabelle.css",
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   337
    hidden: Boolean = true,
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   338
    structural: Boolean = true): String =
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
   339
  {
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   340
    cat_lines(
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   341
      List(header,
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
   342
        output(
66000
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   343
          XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head),
67337
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   344
          hidden = hidden, structural = structural),
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   345
        output(XML.elem("body", body),
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   346
          hidden = hidden, structural = structural)))
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65993
diff changeset
   347
  }
64359
27739e1d7978 more operations;
wenzelm
parents: 64356
diff changeset
   348
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   349
66000
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   350
  /* fonts */
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   351
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   352
  def fonts_url(): String => String =
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   353
    (for (font <- Isabelle_System.fonts(html = true))
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   354
     yield (font.base_name -> Url.print_file(font.file))).toMap
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   355
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   356
  def fonts_dir(prefix: String)(ttf_name: String): String =
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   357
    prefix + "/" + ttf_name
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   358
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   359
  def fonts_css(make_url: String => String = fonts_url()): String =
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   360
  {
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67337
diff changeset
   361
    def font_face(
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67337
diff changeset
   362
        name: String, ttf_name: String, bold: Boolean = false, italic: Boolean = false): String =
66000
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   363
      cat_lines(
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   364
        List(
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   365
          "@font-face {",
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   366
          "  font-family: '" + name + "';",
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   367
          "  src: url('" + make_url(ttf_name) + "') format('truetype');") :::
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   368
        (if (bold) List("  font-weight: bold;") else Nil) :::
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67337
diff changeset
   369
        (if (italic) List("  font-style: italic;") else Nil) :::
66000
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   370
        List("}"))
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   371
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   372
    List(
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   373
      "/* Isabelle fonts */",
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67337
diff changeset
   374
      font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono.ttf"),
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67337
diff changeset
   375
      font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono-Bold.ttf", bold = true),
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67337
diff changeset
   376
      font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono-Oblique.ttf", italic = true),
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67337
diff changeset
   377
      font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono-BoldOblique.ttf", bold = true, italic = true),
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67337
diff changeset
   378
      font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans.ttf"),
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67337
diff changeset
   379
      font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans-Bold.ttf", bold = true),
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67337
diff changeset
   380
      font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans-Oblique.ttf", italic = true),
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67337
diff changeset
   381
      font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans-BoldOblique.ttf", bold = true, italic = true),
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67337
diff changeset
   382
      font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif.ttf"),
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67337
diff changeset
   383
      font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif-Bold.ttf", bold = true),
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67337
diff changeset
   384
      font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif-Oblique.ttf", italic = true),
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67337
diff changeset
   385
      font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif-BoldOblique.ttf", bold = true, italic = true),
66000
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   386
      font_face("Vacuous", "Vacuous.ttf")).mkString("\n\n")
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   387
  }
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   388
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   389
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   390
  /* document directory */
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   391
65998
d07300e8a14d tuned signature;
wenzelm
parents: 65997
diff changeset
   392
  def isabelle_css: Path = Path.explode("~~/etc/isabelle.css")
d07300e8a14d tuned signature;
wenzelm
parents: 65997
diff changeset
   393
66000
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   394
  def write_isabelle_css(dir: Path, make_url: String => String = fonts_dir("fonts"))
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   395
  {
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   396
    File.write(dir + isabelle_css.base,
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   397
      fonts_css(make_url) + "\n\n\n" + File.read(isabelle_css))
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   398
  }
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   399
65836
3b4877fbd9cb more systematic HTML.init_dir with css;
wenzelm
parents: 65834
diff changeset
   400
  def init_dir(dir: Path)
3b4877fbd9cb more systematic HTML.init_dir with css;
wenzelm
parents: 65834
diff changeset
   401
  {
3b4877fbd9cb more systematic HTML.init_dir with css;
wenzelm
parents: 65834
diff changeset
   402
    Isabelle_System.mkdirs(dir)
66000
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65999
diff changeset
   403
    write_isabelle_css(dir)
65836
3b4877fbd9cb more systematic HTML.init_dir with css;
wenzelm
parents: 65834
diff changeset
   404
  }
3b4877fbd9cb more systematic HTML.init_dir with css;
wenzelm
parents: 65834
diff changeset
   405
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   406
  def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
67337
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   407
    css: String = isabelle_css.base_name,
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   408
    hidden: Boolean = true,
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   409
    structural: Boolean = true)
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   410
  {
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   411
    init_dir(dir)
67337
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   412
    File.write(dir + Path.basic(name),
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   413
      output_document(head, body, css = css, hidden = hidden, structural = structural))
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
   414
  }
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
   415
}