isabelle: src/Pure/Thy/html.scala@c6a1031cf925 (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) =>
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	72	s ++= "<"; elem(markup); s ++= ">"
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	73	ts.foreach(tree)
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	74	s ++= "</"; s ++= markup.name; s ++= ">"
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
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	84	/* structured markup */
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	85
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	86	def chapter(body: XML.Body): XML.Elem = XML.elem("h1", body)
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	87	def section(body: XML.Body): XML.Elem = XML.elem("h2", body)
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	88	def subsection(body: XML.Body): XML.Elem = XML.elem("h3", body)
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	89	def subsubsection(body: XML.Body): XML.Elem = XML.elem("h4", body)
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	90	def paragraph(body: XML.Body): XML.Elem = XML.elem("h5", body)
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	91	def subparagraph(body: XML.Body): XML.Elem = XML.elem("h6", body)
c6a1031cf925 support for XML as HTML; wenzelm parents: 62113 diff changeset	92
37200 0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	93
51399 6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	94	/* document */
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	95
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	96	def begin_document(title: String): String =
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	97	"<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	98	"<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	99	"\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	100	"<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	101	"<head>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	102	"<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" +
62113 16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	103	"<title>" + output(title + " (" + Distribution.version + ")") + "</title>\n" +
51399 6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	104	"<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	105	"</head>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	106	"\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	107	"<body>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	108	"<div class=\"head\">" +
62113 16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	109	"<h1>" + output(title) + "</h1>\n"
16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	110
16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	111	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	112
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	113
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	114	/* common markup elements */
33984 c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	115
51402 b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	116	private def session_entry(entry: (String, String)): String =
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	117	{
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	118	val (name, description) = entry
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	119	val descr =
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	120	if (description == "") Nil
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	121	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	122	XML.string_of_tree(
5b2bf7611662 maintain session index on Scala side, for more determistic results; wenzelm parents: 50201 diff changeset	123	XML.elem("li",
5b2bf7611662 maintain session index on Scala side, for more determistic results; wenzelm parents: 50201 diff changeset	124	List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),
51402 b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	125	List(XML.Text(name)))) ::: descr)) + "\n"
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	126	}
34002 cbeeef3aebb3 basic treatment of special control symbols; wenzelm parents: 34000 diff changeset	127
51402 b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	128	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	129	{
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	130	begin_document("Isabelle/" + chapter + " sessions") +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	131	(if (sessions.isEmpty) ""
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	132	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	133	end_document
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	134	}
33984 c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	135	}

author	wenzelm
	Sun, 23 Oct 2016 12:30:57 +0200
changeset 64355	c6a1031cf925
parent 62113	16de2a9b5b3d
child 64356	ebbe7cf0c2b8
permissions	-rw-r--r--