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