isabelle: src/Pure/Thy/html.scala@c41791ad75c3 (annotated)

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	{
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	12	/* encode text with control symbols */
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	13
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 60215 diff changeset	14	val control =
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 60215 diff changeset	15	Map(
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 60215 diff changeset	16	Symbol.sub -> "sub",
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 60215 diff changeset	17	Symbol.sub_decoded -> "sub",
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 60215 diff changeset	18	Symbol.sup -> "sup",
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	19	Symbol.sup_decoded -> "sup",
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 60215 diff changeset	20	Symbol.bold -> "b",
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	21	Symbol.bold_decoded -> "b")
37200 0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	22
64355 c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	23	def output(text: String, s: StringBuilder)
37200 0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	24	{
62113 16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	25	def output_char(c: Char) =
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	26	c match {
64355 c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	27	case '<' => s ++= "<"
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	28	case '>' => s ++= ">"
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	29	case '&' => s ++= "&"
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	30	case '"' => s ++= """
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	31	case '\'' => s ++= "'"
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	32	case '\n' => s ++= "<br/>"
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	33	case _ => s += c
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	34	}
64355 c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	35	def output_chars(str: String) = str.iterator.foreach(output_char(_))
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	36
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 60215 diff changeset	37	var ctrl = ""
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	38	for (sym <- Symbol.iterator(text)) {
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 60215 diff changeset	39	if (control.isDefinedAt(sym)) ctrl = sym
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	40	else {
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 60215 diff changeset	41	control.get(ctrl) match {
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	42	case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
64355 c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	43	s ++= ("<" + elem + ">")
62113 16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	44	output_chars(sym)
64355 c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	45	s ++= ("</" + elem + ">")
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	46	case _ =>
62113 16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	47	output_chars(ctrl)
16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	48	output_chars(sym)
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	49	}
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 60215 diff changeset	50	ctrl = ""
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	51	}
37200 0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	52	}
62113 16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	53	output_chars(ctrl)
64355 c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	54	}
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	55
64355 c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	56	def output(text: String): String = Library.make_string(output(text, _))
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	57
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	58
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	59	/* output XML as HTML */
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	60
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	61	def output(body: XML.Body, s: StringBuilder)
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	62	{
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	63	def attrib(p: (String, String)): Unit =
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	64	{ s ++= " "; s ++= p._1; s ++= "=\""; output(p._2, s); s ++= "\"" }
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	65	def elem(markup: Markup): Unit =
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	66	{ s ++= markup.name; markup.properties.foreach(attrib) }
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	67	def tree(t: XML.Tree): Unit =
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	68	t match {
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	69	case XML.Elem(markup, Nil) =>
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	70	s ++= "<"; elem(markup); s ++= "/>"
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	71	case XML.Elem(markup, ts) =>
64362 8a0fe5469ba0 more readable output: whitespace is insignificant in HTML; wenzelm parents: 64359 diff changeset	72	s ++= "\n<"; elem(markup); s ++= ">"
64355 c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	73	ts.foreach(tree)
64362 8a0fe5469ba0 more readable output: whitespace is insignificant in HTML; wenzelm parents: 64359 diff changeset	74	s ++= "</"; s ++= markup.name; s ++= ">\n"
64355 c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	75	case XML.Text(txt) => output(txt, s)
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	76	}
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	77	body.foreach(tree)
37200 0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	78	}
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	79
64355 c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	80	def output(body: XML.Body): String = Library.make_string(output(body, _))
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	81	def output(tree: XML.Tree): String = output(List(tree))
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	82
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	83
64359 27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	84	/* structured markup operators */
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	85
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	86	def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	87
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	88	class Operator(name: String)
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	89	{ def apply(body: XML.Body): XML.Elem = XML.elem(name, body) }
64356 ebbe7cf0c2b8 tuned; wenzelm parents: 64355 diff changeset	90
64359 27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	91	class Heading(name: String) extends Operator(name)
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	92	{ def apply(txt: String): XML.Elem = super.apply(text(txt)) }
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	93
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	94	val div = new Operator("div")
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	95	val span = new Operator("span")
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	96	val par = new Operator("p")
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	97	val emph = new Operator("em")
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	98	val bold = new Operator("b")
64355 c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	99
64359 27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	100	val title = new Heading("title")
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	101	val chapter = new Heading("h1")
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	102	val section = new Heading("h2")
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	103	val subsection = new Heading("h3")
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	104	val subsubsection = new Heading("h4")
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	105	val paragraph = new Heading("h5")
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	106	val subparagraph = new Heading("h6")
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	107
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	108	def itemize(items: List[XML.Body]): XML.Elem =
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	109	XML.elem("ul", items.map(XML.elem("li", _)))
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	110
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	111	def enumerate(items: List[XML.Body]): XML.Elem =
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	112	XML.elem("ol", items.map(XML.elem("li", _)))
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	113
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	114	def description(items: List[(XML.Body, XML.Body)]): XML.Elem =
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	115	XML.elem("dl", items.flatMap({ case (x, y) => List(XML.elem("dt", x), XML.elem("dd", y)) }))
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	116
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	117	def link(href: String, body: XML.Body = Nil): XML.Elem =
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	118	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	119
37200 0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	120
51399 6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	121	/* document */
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	122
64359 27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	123	val header: String =
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	124	"""<?xml version="1.0" encoding="utf-8" ?>
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	125	<!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	126	<html xmlns="http://www.w3.org/1999/xhtml">"""
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	127
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	128	val head_meta: XML.Elem =
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	129	XML.Elem(Markup("meta",
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	130	List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil)
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	131
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	132	def output_document(head: XML.Body, body: XML.Body): String =
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	133	cat_lines(
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	134	List(header,
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	135	output(XML.elem("head", head_meta :: head)),
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	136	output(XML.elem("body", body))))
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	137
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	138
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	139	/* Isabelle document */
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	140
51399 6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	141	def begin_document(title: String): String =
64359 27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	142	header + "\n" +
27739e1d7978 more operations; wenzelm parents: 64356 diff changeset	143	"<head>\n" + output(head_meta) + "\n" +
62113 16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	144	"<title>" + output(title + " (" + Distribution.version + ")") + "</title>\n" +
51399 6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	145	"<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	146	"</head>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	147	"\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	148	"<body>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	149	"<div class=\"head\">" +
62113 16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	150	"<h1>" + output(title) + "</h1>\n"
16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	151
16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	152	val end_document = "\n</div>\n</body>\n</html>\n"
51399 6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	153
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	154
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	155	/* common markup elements */
33984 c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	156
51402 b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	157	private def session_entry(entry: (String, String)): String =
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	158	{
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	159	val (name, description) = entry
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	160	val descr =
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	161	if (description == "") Nil
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	162	else List(XML.elem("br"), XML.elem("pre", List(XML.Text(description))))
50707 5b2bf7611662 maintain session index on Scala side, for more determistic results; wenzelm parents: 50201 diff changeset	163	XML.string_of_tree(
5b2bf7611662 maintain session index on Scala side, for more determistic results; wenzelm parents: 50201 diff changeset	164	XML.elem("li",
5b2bf7611662 maintain session index on Scala side, for more determistic results; wenzelm parents: 50201 diff changeset	165	List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),
51402 b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	166	List(XML.Text(name)))) ::: descr)) + "\n"
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	167	}
34002 cbeeef3aebb3 basic treatment of special control symbols; wenzelm parents: 34000 diff changeset	168
51402 b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	169	def chapter_index(chapter: String, sessions: List[(String, String)]): String =
51399 6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	170	{
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	171	begin_document("Isabelle/" + chapter + " sessions") +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	172	(if (sessions.isEmpty) ""
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	173	else "<div class=\"sessions\"><ul>\n" + sessions.map(session_entry(_)).mkString + "</ul>") +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	174	end_document
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	175	}
33984 c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	176	}

author	wenzelm
	Wed, 12 Apr 2017 17:48:19 +0200
changeset 65468	c41791ad75c3
parent 64362	8a0fe5469ba0
child 65753	787e5ee6ef53
permissions	-rw-r--r--