/* Title: Pure/Thy/html.scala
Author: Makarius
HTML presentation elements.
*/
package isabelle
object HTML
{
/* encode text with control symbols */
val control =
Map(
Symbol.sub -> "sub",
Symbol.sub_decoded -> "sub",
Symbol.sup -> "sup",
Symbol.sup_decoded -> "sup",
Symbol.bold -> "b",
Symbol.bold_decoded -> "b")
def output(text: String, s: StringBuilder)
{
def output_char(c: Char) =
c match {
case '<' => s ++= "<"
case '>' => s ++= ">"
case '&' => s ++= "&"
case '"' => s ++= """
case '\'' => s ++= "'"
case '\n' => s ++= "<br/>"
case _ => s += c
}
def output_chars(str: String) = str.iterator.foreach(output_char(_))
var ctrl = ""
for (sym <- Symbol.iterator(text)) {
if (control.isDefinedAt(sym)) ctrl = sym
else {
control.get(ctrl) match {
case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
s ++= ("<" + elem + ">")
output_chars(sym)
s ++= ("</" + elem + ">")
case _ =>
output_chars(ctrl)
output_chars(sym)
}
ctrl = ""
}
}
output_chars(ctrl)
}
def output(text: String): String = Library.make_string(output(text, _))
/* output XML as HTML */
private val structural_elements =
Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6",
"ul", "ol", "dl", "li", "dt", "dd")
def output(body: XML.Body, s: StringBuilder)
{
def attrib(p: (String, String)): Unit =
{ s ++= " "; s ++= p._1; s ++= "=\""; output(p._2, s); s ++= "\"" }
def elem(markup: Markup): Unit =
{ s ++= markup.name; markup.properties.foreach(attrib) }
def tree(t: XML.Tree): Unit =
t match {
case XML.Elem(markup, Nil) =>
s ++= "<"; elem(markup); s ++= "/>"
case XML.Elem(markup, ts) =>
if (structural_elements(markup.name)) s += '\n'
s ++= "<"; elem(markup); s ++= ">"
ts.foreach(tree)
s ++= "</"; s ++= markup.name; s ++= ">"
if (structural_elements(markup.name)) s += '\n'
case XML.Text(txt) => output(txt, s)
}
body.foreach(tree)
}
def output(body: XML.Body): String = Library.make_string(output(body, _))
def output(tree: XML.Tree): String = output(List(tree))
/* attributes */
def id(s: String): XML.Attribute = ("id" -> s)
def width(w: Int): XML.Attribute = ("width" -> w.toString)
def height(h: Int): XML.Attribute = ("height" -> h.toString)
/* structured markup operators */
def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
val break: XML.Body = List(XML.elem("br"))
class Operator(name: String)
{ def apply(body: XML.Body): XML.Elem = XML.elem(name, body) }
class Heading(name: String) extends Operator(name)
{ def apply(txt: String): XML.Elem = super.apply(text(txt)) }
val div = new Operator("div")
val span = new Operator("span")
val pre = new Operator("pre")
val par = new Operator("p")
val emph = new Operator("em")
val bold = new Operator("b")
val code = new Operator("code")
val title = new Heading("title")
val chapter = new Heading("h1")
val section = new Heading("h2")
val subsection = new Heading("h3")
val subsubsection = new Heading("h4")
val paragraph = new Heading("h5")
val subparagraph = new Heading("h6")
def itemize(items: List[XML.Body]): XML.Elem =
XML.elem("ul", items.map(XML.elem("li", _)))
def enumerate(items: List[XML.Body]): XML.Elem =
XML.elem("ol", items.map(XML.elem("li", _)))
def description(items: List[(XML.Body, XML.Body)]): XML.Elem =
XML.elem("dl", items.flatMap({ case (x, y) => List(XML.elem("dt", x), XML.elem("dd", y)) }))
def link(href: String, body: XML.Body = Nil): XML.Elem =
XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body)
def image(src: String, alt: String = ""): XML.Elem =
XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
/* document */
val header: String =
"""<?xml version="1.0" encoding="utf-8" ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">"""
val head_meta: XML.Elem =
XML.Elem(Markup("meta",
List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil)
def head_css(css: String): XML.Elem =
XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> css)), Nil)
def output_document(head: XML.Body, body: XML.Body, css: String = "isabelle.css"): String =
cat_lines(
List(header,
output(XML.elem("head", head_meta :: (if (css == "") Nil else List(head_css(css))) ::: head)),
output(XML.elem("body", body))))
def init_dir(dir: Path)
{
Isabelle_System.mkdirs(dir)
File.copy(Path.explode("~~/etc/isabelle.css"), dir)
}
/* Isabelle document */
def begin_document(title: String): String =
header + "\n" +
"<head>\n" + output(head_meta) + "\n" +
"<title>" + output(title + " (" + Distribution.version + ")") + "</title>\n" +
"<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" +
"</head>\n" +
"\n" +
"<body>\n" +
"<div class=\"head\">" +
"<h1>" + output(title) + "</h1>\n"
val end_document = "\n</div>\n</body>\n</html>\n"
/* common markup elements */
private def session_entry(entry: (String, String)): String =
{
val (name, description) = entry
val descr = if (description == "") Nil else break ::: List(pre(text(description)))
XML.string_of_tree(
XML.elem("li",
List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),
List(XML.Text(name)))) ::: descr)) + "\n"
}
def chapter_index(chapter: String, sessions: List[(String, String)]): String =
{
begin_document("Isabelle/" + chapter + " sessions") +
(if (sessions.isEmpty) ""
else "<div class=\"sessions\"><ul>\n" + sessions.map(session_entry(_)).mkString + "</ul>") +
end_document
}
}