src/Pure/Thy/html.scala
author wenzelm
Thu Nov 02 10:16:22 2017 +0100 (19 months ago)
changeset 66987 352b23c97ac8
parent 66212 f41396c15bb1
child 67255 f1f983484878
permissions -rw-r--r--
support focus_session, for much faster startup of Isabelle/jEdit;
more options for "isabelle jedit";
wenzelm@33984
     1
/*  Title:      Pure/Thy/html.scala
wenzelm@33984
     2
    Author:     Makarius
wenzelm@33984
     3
wenzelm@50707
     4
HTML presentation elements.
wenzelm@33984
     5
*/
wenzelm@33984
     6
wenzelm@33984
     7
package isabelle
wenzelm@33984
     8
wenzelm@55618
     9
wenzelm@33984
    10
object HTML
wenzelm@33984
    11
{
wenzelm@65997
    12
  /* output text with control symbols */
wenzelm@59063
    13
wenzelm@65997
    14
  private val control =
wenzelm@65997
    15
    Map(
wenzelm@65997
    16
      Symbol.sub -> "sub", Symbol.sub_decoded -> "sub",
wenzelm@65997
    17
      Symbol.sup -> "sup", Symbol.sup_decoded -> "sup",
wenzelm@65997
    18
      Symbol.bold -> "b", Symbol.bold_decoded -> "b")
wenzelm@65997
    19
wenzelm@65997
    20
  private val control_block =
wenzelm@62104
    21
    Map(
wenzelm@65997
    22
      Symbol.bsub -> "<sub>", Symbol.bsub_decoded -> "<sub>",
wenzelm@65997
    23
      Symbol.esub -> "</sub>", Symbol.esub_decoded -> "</sub>",
wenzelm@65997
    24
      Symbol.bsup -> "<sup>", Symbol.bsup_decoded -> "<sup>",
wenzelm@65997
    25
      Symbol.esup -> "</sup>", Symbol.esup_decoded -> "</sup>")
wenzelm@65997
    26
wenzelm@65997
    27
  def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym)
wenzelm@65997
    28
wenzelm@66018
    29
  def output_char_permissive(c: Char, s: StringBuilder)
wenzelm@65997
    30
  {
wenzelm@66018
    31
    c match {
wenzelm@66018
    32
      case '<' => s ++= "&lt;"
wenzelm@66018
    33
      case '>' => s ++= "&gt;"
wenzelm@66018
    34
      case '&' => s ++= "&amp;"
wenzelm@66018
    35
      case _ => s += c
wenzelm@66018
    36
    }
wenzelm@66018
    37
  }
wenzelm@66018
    38
wenzelm@66018
    39
  def output(text: String, s: StringBuilder, hidden: Boolean, permissive: Boolean)
wenzelm@66018
    40
  {
wenzelm@66018
    41
    def output_char(c: Char): Unit =
wenzelm@66018
    42
      if (permissive) output_char_permissive(c, s)
wenzelm@66018
    43
      else XML.output_char(c, s)
wenzelm@66018
    44
wenzelm@66018
    45
    def output_string(str: String): Unit =
wenzelm@66018
    46
      str.iterator.foreach(output_char)
wenzelm@66018
    47
wenzelm@65997
    48
    def output_hidden(body: => Unit): Unit =
wenzelm@65997
    49
      if (hidden) { s ++= "<span class=\"hidden\">"; body; s ++= "</span>" }
wenzelm@37200
    50
wenzelm@65997
    51
    def output_symbol(sym: Symbol.Symbol): Unit =
wenzelm@65997
    52
      if (sym != "") {
wenzelm@65997
    53
        control_block.get(sym) match {
wenzelm@65997
    54
          case Some(html) if html.startsWith("</") =>
wenzelm@66018
    55
            s ++= html; output_hidden(output_string(sym))
wenzelm@65997
    56
          case Some(html) =>
wenzelm@66018
    57
            output_hidden(output_string(sym)); s ++= html
wenzelm@65997
    58
          case None =>
wenzelm@66018
    59
            output_string(sym)
wenzelm@65997
    60
        }
wenzelm@65997
    61
      }
wenzelm@59063
    62
wenzelm@62104
    63
    var ctrl = ""
wenzelm@59063
    64
    for (sym <- Symbol.iterator(text)) {
wenzelm@65997
    65
      if (is_control(sym)) { output_symbol(ctrl); ctrl = sym }
wenzelm@59063
    66
      else {
wenzelm@62104
    67
        control.get(ctrl) match {
wenzelm@66006
    68
          case Some(elem) if Symbol.is_controllable(sym) =>
wenzelm@65997
    69
            output_hidden(output_symbol(ctrl))
wenzelm@65991
    70
            s += '<'; s ++= elem; s += '>'
wenzelm@65997
    71
            output_symbol(sym)
wenzelm@65991
    72
            s ++= "</"; s ++= elem; s += '>'
wenzelm@59063
    73
          case _ =>
wenzelm@65997
    74
            output_symbol(ctrl)
wenzelm@65997
    75
            output_symbol(sym)
wenzelm@59063
    76
        }
wenzelm@62104
    77
        ctrl = ""
wenzelm@59063
    78
      }
wenzelm@37200
    79
    }
wenzelm@65997
    80
    output_symbol(ctrl)
wenzelm@64355
    81
  }
wenzelm@59063
    82
wenzelm@66018
    83
  def output(text: String): String =
wenzelm@66018
    84
    Library.make_string(output(text, _, hidden = false, permissive = true))
wenzelm@64355
    85
wenzelm@64355
    86
wenzelm@64355
    87
  /* output XML as HTML */
wenzelm@64355
    88
wenzelm@65834
    89
  private val structural_elements =
wenzelm@65834
    90
    Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6",
wenzelm@65834
    91
      "ul", "ol", "dl", "li", "dt", "dd")
wenzelm@65834
    92
wenzelm@65997
    93
  def output(body: XML.Body, s: StringBuilder, hidden: Boolean)
wenzelm@64355
    94
  {
wenzelm@65991
    95
    def elem(markup: Markup)
wenzelm@65991
    96
    {
wenzelm@65991
    97
      s ++= markup.name
wenzelm@65991
    98
      for ((a, b) <- markup.properties) {
wenzelm@66018
    99
        s += ' '
wenzelm@66018
   100
        s ++= a
wenzelm@66018
   101
        s += '='
wenzelm@66018
   102
        s += '"'
wenzelm@66018
   103
        output(b, s, hidden = hidden, permissive = false)
wenzelm@66018
   104
        s += '"'
wenzelm@65991
   105
      }
wenzelm@65991
   106
    }
wenzelm@64355
   107
    def tree(t: XML.Tree): Unit =
wenzelm@64355
   108
      t match {
wenzelm@64355
   109
        case XML.Elem(markup, Nil) =>
wenzelm@65991
   110
          s += '<'; elem(markup); s ++= "/>"
wenzelm@64355
   111
        case XML.Elem(markup, ts) =>
wenzelm@65834
   112
          if (structural_elements(markup.name)) s += '\n'
wenzelm@65991
   113
          s += '<'; elem(markup); s += '>'
wenzelm@64355
   114
          ts.foreach(tree)
wenzelm@65991
   115
          s ++= "</"; s ++= markup.name; s += '>'
wenzelm@65834
   116
          if (structural_elements(markup.name)) s += '\n'
wenzelm@65997
   117
        case XML.Text(txt) =>
wenzelm@66018
   118
          output(txt, s, hidden = hidden, permissive = true)
wenzelm@64355
   119
      }
wenzelm@64355
   120
    body.foreach(tree)
wenzelm@37200
   121
  }
wenzelm@37200
   122
wenzelm@65997
   123
  def output(body: XML.Body, hidden: Boolean): String =
wenzelm@65997
   124
    Library.make_string(output(body, _, hidden))
wenzelm@65997
   125
wenzelm@65997
   126
  def output(tree: XML.Tree, hidden: Boolean): String =
wenzelm@65997
   127
    output(List(tree), hidden)
wenzelm@64355
   128
wenzelm@64355
   129
wenzelm@65753
   130
  /* attributes */
wenzelm@65753
   131
wenzelm@65992
   132
  class Attribute(val name: String, value: String)
wenzelm@65992
   133
  {
wenzelm@65992
   134
    def xml: XML.Attribute = name -> value
wenzelm@65992
   135
    def apply(elem: XML.Elem): XML.Elem = elem + xml
wenzelm@65992
   136
  }
wenzelm@65942
   137
wenzelm@65992
   138
  def id(s: String): Attribute = new Attribute("id", s)
wenzelm@65993
   139
  def class_(name: String): Attribute = new Attribute("class", name)
wenzelm@65946
   140
wenzelm@65992
   141
  def width(w: Int): Attribute = new Attribute("width", w.toString)
wenzelm@65992
   142
  def height(h: Int): Attribute = new Attribute("height", h.toString)
wenzelm@65946
   143
  def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem))
wenzelm@65753
   144
wenzelm@65753
   145
wenzelm@64359
   146
  /* structured markup operators */
wenzelm@64359
   147
wenzelm@64359
   148
  def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
wenzelm@65753
   149
  val break: XML.Body = List(XML.elem("br"))
wenzelm@64359
   150
wenzelm@65992
   151
  class Operator(val name: String)
wenzelm@65992
   152
  {
wenzelm@65992
   153
    def apply(body: XML.Body): XML.Elem = XML.elem(name, body)
wenzelm@65992
   154
    def apply(att: Attribute, body: XML.Body): XML.Elem = att(apply(body))
wenzelm@65993
   155
    def apply(c: String, body: XML.Body): XML.Elem = apply(class_(c), body)
wenzelm@65992
   156
  }
wenzelm@64356
   157
wenzelm@64359
   158
  class Heading(name: String) extends Operator(name)
wenzelm@65992
   159
  {
wenzelm@65992
   160
    def apply(txt: String): XML.Elem = super.apply(text(txt))
wenzelm@65992
   161
    def apply(att: Attribute, txt: String): XML.Elem = super.apply(att, text(txt))
wenzelm@65992
   162
    def apply(c: String, txt: String): XML.Elem = super.apply(c, text(txt))
wenzelm@65992
   163
  }
wenzelm@64359
   164
wenzelm@64359
   165
  val div = new Operator("div")
wenzelm@64359
   166
  val span = new Operator("span")
wenzelm@65753
   167
  val pre = new Operator("pre")
wenzelm@64359
   168
  val par = new Operator("p")
wenzelm@64359
   169
  val emph = new Operator("em")
wenzelm@64359
   170
  val bold = new Operator("b")
wenzelm@65771
   171
  val code = new Operator("code")
wenzelm@64355
   172
wenzelm@64359
   173
  val title = new Heading("title")
wenzelm@64359
   174
  val chapter = new Heading("h1")
wenzelm@64359
   175
  val section = new Heading("h2")
wenzelm@64359
   176
  val subsection = new Heading("h3")
wenzelm@64359
   177
  val subsubsection = new Heading("h4")
wenzelm@64359
   178
  val paragraph = new Heading("h5")
wenzelm@64359
   179
  val subparagraph = new Heading("h6")
wenzelm@64359
   180
wenzelm@64359
   181
  def itemize(items: List[XML.Body]): XML.Elem =
wenzelm@64359
   182
    XML.elem("ul", items.map(XML.elem("li", _)))
wenzelm@64359
   183
wenzelm@64359
   184
  def enumerate(items: List[XML.Body]): XML.Elem =
wenzelm@64359
   185
    XML.elem("ol", items.map(XML.elem("li", _)))
wenzelm@64359
   186
wenzelm@64359
   187
  def description(items: List[(XML.Body, XML.Body)]): XML.Elem =
wenzelm@64359
   188
    XML.elem("dl", items.flatMap({ case (x, y) => List(XML.elem("dt", x), XML.elem("dd", y)) }))
wenzelm@64359
   189
wenzelm@64359
   190
  def link(href: String, body: XML.Body = Nil): XML.Elem =
wenzelm@64359
   191
    XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body)
wenzelm@64355
   192
wenzelm@65753
   193
  def image(src: String, alt: String = ""): XML.Elem =
wenzelm@65753
   194
    XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
wenzelm@65753
   195
wenzelm@66040
   196
  def source(body: XML.Body): XML.Elem = pre("source", body)
wenzelm@66040
   197
  def source(src: String): XML.Elem = source(text(src))
wenzelm@65988
   198
wenzelm@65941
   199
  def style(s: String): XML.Elem = XML.elem("style", text(s))
wenzelm@66000
   200
  def style_file(href: String): XML.Elem =
wenzelm@66000
   201
    XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)
wenzelm@66212
   202
  def style_file(path: Path): XML.Elem = style_file(Url.print_file(path.file))
wenzelm@66000
   203
wenzelm@66210
   204
  def script(s: String): XML.Elem = XML.elem("script", text(s))
wenzelm@66210
   205
  def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil)
wenzelm@66212
   206
  def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file))
wenzelm@66212
   207
wenzelm@37200
   208
wenzelm@65892
   209
  /* messages */
wenzelm@65892
   210
wenzelm@65939
   211
  // background
wenzelm@65993
   212
  val writeln_message: Attribute = class_("writeln_message")
wenzelm@65993
   213
  val warning_message: Attribute = class_("warning_message")
wenzelm@65993
   214
  val error_message: Attribute = class_("error_message")
wenzelm@65892
   215
wenzelm@65939
   216
  // underline
wenzelm@65993
   217
  val writeln: Attribute = class_("writeln")
wenzelm@65993
   218
  val warning: Attribute = class_("warning")
wenzelm@65993
   219
  val error: Attribute = class_("error")
wenzelm@65892
   220
wenzelm@65944
   221
wenzelm@65944
   222
  /* tooltips */
wenzelm@65944
   223
wenzelm@65944
   224
  def tooltip(item: XML.Body, tip: XML.Body): XML.Elem =
wenzelm@65992
   225
    span(item ::: List(div("tooltip", tip)))
wenzelm@65944
   226
wenzelm@65944
   227
  def tooltip_errors(item: XML.Body, msgs: List[XML.Body]): XML.Elem =
wenzelm@65944
   228
    HTML.error(tooltip(item, msgs.map(msg => error_message(pre(msg)))))
wenzelm@65892
   229
wenzelm@65892
   230
wenzelm@66196
   231
  /* GUI elements */
wenzelm@66196
   232
wenzelm@66196
   233
  object GUI
wenzelm@66196
   234
  {
wenzelm@66196
   235
    private def optional_value(text: String): XML.Attributes =
wenzelm@66196
   236
      proper_string(text).map(a => "value" -> a).toList
wenzelm@66196
   237
wenzelm@66196
   238
    private def optional_name(name: String): XML.Attributes =
wenzelm@66196
   239
      proper_string(name).map(a => "name" -> a).toList
wenzelm@66196
   240
wenzelm@66196
   241
    private def optional_title(tooltip: String): XML.Attributes =
wenzelm@66196
   242
      proper_string(tooltip).map(a => "title" -> a).toList
wenzelm@66196
   243
wenzelm@66196
   244
    private def optional_submit(submit: Boolean): XML.Attributes =
wenzelm@66196
   245
      if (submit) List("onChange" -> "this.form.submit()") else Nil
wenzelm@66196
   246
wenzelm@66196
   247
    private def optional_checked(selected: Boolean): XML.Attributes =
wenzelm@66196
   248
      if (selected) List("checked" -> "") else Nil
wenzelm@66196
   249
wenzelm@66196
   250
    private def optional_action(action: String): XML.Attributes =
wenzelm@66196
   251
      proper_string(action).map(a => "action" -> a).toList
wenzelm@66196
   252
wenzelm@66210
   253
    private def optional_onclick(script: String): XML.Attributes =
wenzelm@66210
   254
      proper_string(script).map(a => "onclick" -> a).toList
wenzelm@66210
   255
wenzelm@66210
   256
    private def optional_onchange(script: String): XML.Attributes =
wenzelm@66210
   257
      proper_string(script).map(a => "onchange" -> a).toList
wenzelm@66210
   258
wenzelm@66210
   259
    def button(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false,
wenzelm@66210
   260
        script: String = ""): XML.Elem =
wenzelm@66196
   261
      XML.Elem(
wenzelm@66196
   262
        Markup("button",
wenzelm@66196
   263
          List("type" -> (if (submit) "submit" else "button"), "value" -> "true") :::
wenzelm@66210
   264
          optional_name(name) ::: optional_title(tooltip) ::: optional_onclick(script)), body)
wenzelm@66196
   265
wenzelm@66196
   266
    def checkbox(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false,
wenzelm@66210
   267
        selected: Boolean = false, script: String = ""): XML.Elem =
wenzelm@66196
   268
      XML.elem("label",
wenzelm@66196
   269
        XML.elem(
wenzelm@66196
   270
          Markup("input",
wenzelm@66196
   271
            List("type" -> "checkbox", "value" -> "true") ::: optional_name(name) :::
wenzelm@66196
   272
              optional_title(tooltip) ::: optional_submit(submit) :::
wenzelm@66210
   273
              optional_checked(selected) ::: optional_onchange(script))) :: body)
wenzelm@66196
   274
wenzelm@66196
   275
    def text_field(columns: Int = 0, text: String = "", name: String = "", tooltip: String = "",
wenzelm@66210
   276
        submit: Boolean = false, script: String = ""): XML.Elem =
wenzelm@66196
   277
      XML.elem(Markup("input",
wenzelm@66196
   278
        List("type" -> "text") :::
wenzelm@66196
   279
          (if (columns > 0) List("size" -> columns.toString) else Nil) :::
wenzelm@66210
   280
          optional_value(text) ::: optional_name(name) ::: optional_title(tooltip) :::
wenzelm@66210
   281
          optional_submit(submit) ::: optional_onchange(script)))
wenzelm@66196
   282
wenzelm@66196
   283
    def parameter(text: String = "", name: String = ""): XML.Elem =
wenzelm@66196
   284
      XML.elem(
wenzelm@66196
   285
        Markup("input", List("type" -> "hidden") ::: optional_value(text) ::: optional_name(name)))
wenzelm@66196
   286
wenzelm@66209
   287
    def form(body: XML.Body, name: String = "", action: String = "", http_post: Boolean = false)
wenzelm@66209
   288
        : XML.Elem =
wenzelm@66209
   289
      XML.Elem(
wenzelm@66209
   290
        Markup("form", optional_name(name) ::: optional_action(action) :::
wenzelm@66209
   291
          (if (http_post) List("method" -> "post") else Nil)), body)
wenzelm@66196
   292
  }
wenzelm@66196
   293
wenzelm@66196
   294
wenzelm@66200
   295
  /* GUI layout */
wenzelm@66200
   296
wenzelm@66200
   297
  object Wrap_Panel
wenzelm@66200
   298
  {
wenzelm@66200
   299
    object Alignment extends Enumeration
wenzelm@66200
   300
    {
wenzelm@66200
   301
      val left, right, center = Value
wenzelm@66200
   302
    }
wenzelm@66200
   303
wenzelm@66200
   304
    def apply(contents: List[XML.Elem], name: String = "", action: String = "",
wenzelm@66206
   305
      alignment: Alignment.Value = Alignment.right): XML.Elem =
wenzelm@66200
   306
    {
wenzelm@66200
   307
      val body = Library.separate(XML.Text(" "), contents)
wenzelm@66200
   308
      GUI.form(List(div(body) + ("style" -> ("text-align: " + alignment))),
wenzelm@66200
   309
        name = name, action = action)
wenzelm@66200
   310
    }
wenzelm@66200
   311
  }
wenzelm@66200
   312
wenzelm@66200
   313
wenzelm@51399
   314
  /* document */
wenzelm@51399
   315
wenzelm@64359
   316
  val header: String =
wenzelm@64359
   317
    """<?xml version="1.0" encoding="utf-8" ?>
wenzelm@64359
   318
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
wenzelm@64359
   319
<html xmlns="http://www.w3.org/1999/xhtml">"""
wenzelm@64359
   320
wenzelm@64359
   321
  val head_meta: XML.Elem =
wenzelm@64359
   322
    XML.Elem(Markup("meta",
wenzelm@64359
   323
      List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil)
wenzelm@64359
   324
wenzelm@65997
   325
  def output_document(head: XML.Body, body: XML.Body,
wenzelm@65997
   326
    css: String = "isabelle.css", hidden: Boolean = true): String =
wenzelm@65997
   327
  {
wenzelm@64359
   328
    cat_lines(
wenzelm@64359
   329
      List(header,
wenzelm@65997
   330
        output(
wenzelm@66000
   331
          XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head),
wenzelm@65997
   332
          hidden = hidden),
wenzelm@65997
   333
        output(XML.elem("body", body), hidden = hidden)))
wenzelm@65997
   334
  }
wenzelm@64359
   335
wenzelm@65838
   336
wenzelm@66000
   337
  /* fonts */
wenzelm@66000
   338
wenzelm@66000
   339
  def fonts_url(): String => String =
wenzelm@66000
   340
    (for (font <- Isabelle_System.fonts(html = true))
wenzelm@66000
   341
     yield (font.base_name -> Url.print_file(font.file))).toMap
wenzelm@66000
   342
wenzelm@66000
   343
  def fonts_dir(prefix: String)(ttf_name: String): String =
wenzelm@66000
   344
    prefix + "/" + ttf_name
wenzelm@66000
   345
wenzelm@66000
   346
  def fonts_css(make_url: String => String = fonts_url()): String =
wenzelm@66000
   347
  {
wenzelm@66000
   348
    def font_face(name: String, ttf_name: String, bold: Boolean = false): String =
wenzelm@66000
   349
      cat_lines(
wenzelm@66000
   350
        List(
wenzelm@66000
   351
          "@font-face {",
wenzelm@66000
   352
          "  font-family: '" + name + "';",
wenzelm@66000
   353
          "  src: url('" + make_url(ttf_name) + "') format('truetype');") :::
wenzelm@66000
   354
        (if (bold) List("  font-weight: bold;") else Nil) :::
wenzelm@66000
   355
        List("}"))
wenzelm@66000
   356
wenzelm@66000
   357
    List(
wenzelm@66000
   358
      "/* Isabelle fonts */",
wenzelm@66000
   359
      font_face("IsabelleText", "IsabelleText.ttf"),
wenzelm@66000
   360
      font_face("IsabelleText", "IsabelleTextBold.ttf", bold = true),
wenzelm@66000
   361
      font_face("Vacuous", "Vacuous.ttf")).mkString("\n\n")
wenzelm@66000
   362
  }
wenzelm@66000
   363
wenzelm@66000
   364
wenzelm@65838
   365
  /* document directory */
wenzelm@65838
   366
wenzelm@65998
   367
  def isabelle_css: Path = Path.explode("~~/etc/isabelle.css")
wenzelm@65998
   368
wenzelm@66000
   369
  def write_isabelle_css(dir: Path, make_url: String => String = fonts_dir("fonts"))
wenzelm@66000
   370
  {
wenzelm@66000
   371
    File.write(dir + isabelle_css.base,
wenzelm@66000
   372
      fonts_css(make_url) + "\n\n\n" + File.read(isabelle_css))
wenzelm@66000
   373
  }
wenzelm@66000
   374
wenzelm@65836
   375
  def init_dir(dir: Path)
wenzelm@65836
   376
  {
wenzelm@65836
   377
    Isabelle_System.mkdirs(dir)
wenzelm@66000
   378
    write_isabelle_css(dir)
wenzelm@65836
   379
  }
wenzelm@65836
   380
wenzelm@65838
   381
  def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
wenzelm@65999
   382
    css: String = isabelle_css.base_name, hidden: Boolean = true)
wenzelm@65838
   383
  {
wenzelm@65838
   384
    init_dir(dir)
wenzelm@65997
   385
    File.write(dir + Path.basic(name), output_document(head, body, css = css, hidden = hidden))
wenzelm@65838
   386
  }
wenzelm@33984
   387
}