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