isabelle: src/Pure/Thy/html.scala@83841a5c0897 (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
62113 16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	23	def output(text: String): String =
37200 0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	24	{
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	25	val result = new StringBuilder
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	26
62113 16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	27	def output_char(c: Char) =
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	28	c match {
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	29	case '<' => result ++= "<"
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	30	case '>' => result ++= ">"
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	31	case '&' => result ++= "&"
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	32	case '"' => result ++= """
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	33	case '\'' => result ++= "'"
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	34	case '\n' => result ++= "<br/>"
60215 5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA; wenzelm parents: 60033 diff changeset	35	case _ => result += c
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	36	}
62113 16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	37	def output_chars(s: String) = s.iterator.foreach(output_char(_))
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	38
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 60215 diff changeset	39	var ctrl = ""
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	40	for (sym <- Symbol.iterator(text)) {
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 60215 diff changeset	41	if (control.isDefinedAt(sym)) ctrl = sym
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	42	else {
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 60215 diff changeset	43	control.get(ctrl) match {
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	44	case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	45	result ++= ("<" + elem + ">")
62113 16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	46	output_chars(sym)
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	47	result ++= ("</" + elem + ">")
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	48	case _ =>
62113 16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	49	output_chars(ctrl)
16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	50	output_chars(sym)
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	51	}
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 60215 diff changeset	52	ctrl = ""
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	53	}
37200 0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	54	}
62113 16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	55	output_chars(ctrl)
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	56
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	57	result.toString
37200 0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	58	}
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	59
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	60
51399 6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	61	/* document */
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	62
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	63	def begin_document(title: String): String =
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	64	"<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	65	"<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	66	"\"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	67	"<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	68	"<head>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	69	"<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" +
62113 16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	70	"<title>" + output(title + " (" + Distribution.version + ")") + "</title>\n" +
51399 6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	71	"<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	72	"</head>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	73	"\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	74	"<body>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	75	"<div class=\"head\">" +
62113 16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	76	"<h1>" + output(title) + "</h1>\n"
16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	77
16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 62104 diff changeset	78	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	79
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	80
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	81	/* common markup elements */
33984 c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	82
51402 b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	83	private def session_entry(entry: (String, String)): String =
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	84	{
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	85	val (name, description) = entry
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	86	val descr =
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	87	if (description == "") Nil
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	88	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	89	XML.string_of_tree(
5b2bf7611662 maintain session index on Scala side, for more determistic results; wenzelm parents: 50201 diff changeset	90	XML.elem("li",
5b2bf7611662 maintain session index on Scala side, for more determistic results; wenzelm parents: 50201 diff changeset	91	List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),
51402 b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	92	List(XML.Text(name)))) ::: descr)) + "\n"
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	93	}
34002 cbeeef3aebb3 basic treatment of special control symbols; wenzelm parents: 34000 diff changeset	94
51402 b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	95	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	96	{
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	97	begin_document("Isabelle/" + chapter + " sessions") +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	98	(if (sessions.isEmpty) ""
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	99	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	100	end_document
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	101	}
33984 c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	102	}

author	blanchet
	Tue, 06 Sep 2016 11:55:39 +0200
changeset 63801	83841a5c0897
parent 62113	16de2a9b5b3d
child 64355	c6a1031cf925
permissions	-rw-r--r--