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

33984 c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	1	/* Title: Pure/Thy/html.scala
56748 10b52ca3b4a2 clarified PIDE modules; wenzelm parents: 56745 diff changeset	2	Module: PIDE
33984 c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	3	Author: Makarius
c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	4
50707 5b2bf7611662 maintain session index on Scala side, for more determistic results; wenzelm parents: 50201 diff changeset	5	HTML presentation elements.
33984 c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	6	*/
c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	7
c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	8	package isabelle
c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	9
55618 995162143ef4 tuned imports; wenzelm parents: 54379 diff changeset	10
33984 c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	11	object HTML
c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	12	{
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	13	/* encode text with control symbols */
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	14
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	15	val control_decoded =
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	16	Map(Symbol.sub_decoded -> "sub",
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	17	Symbol.sup_decoded -> "sup",
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	18	Symbol.bold_decoded -> "b")
37200 0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	19
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	20	def encode(text: String): String =
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	21	{
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	22	val result = new StringBuilder
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	23
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	24	def encode_char(c: Char) =
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	25	c match {
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	26	case '<' => result ++= "<"
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	27	case '>' => result ++= ">"
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	28	case '&' => result ++= "&"
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 '\n' => result ++= "<br/>"
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	32	case c => result += c
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	33	}
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	34	def encode_chars(s: String) = s.iterator.foreach(encode_char(_))
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	35
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	36	var control = ""
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	37	for (sym <- Symbol.iterator(text)) {
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	38	if (control_decoded.isDefinedAt(sym)) control = sym
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	39	else {
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	40	control_decoded.get(control) match {
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	41	case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	42	result ++= ("<" + elem + ">")
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	43	encode_chars(sym)
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	44	result ++= ("</" + elem + ">")
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	45	case _ =>
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	46	encode_chars(control)
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	47	encode_chars(sym)
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	48	}
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	49	control = ""
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	50	}
37200 0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	51	}
59063 b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	52	encode_chars(control)
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	53
b3c45d0e4fe1 encode text with control symbols; wenzelm parents: 56748 diff changeset	54	result.toString
37200 0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	55	}
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	56
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	57
51399 6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	58	/* document */
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	59
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	60	val end_document = "\n</div>\n</body>\n</html>\n"
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	61
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	62	def begin_document(title: String): String =
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	63	"<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	64	"<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	65	"\"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	66	"<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	67	"<head>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	68	"<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	69	"<title>" + encode(title) + "</title>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	70	"<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	71	"</head>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	72	"\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	73	"<body>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	74	"<div class=\"head\">" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	75	"<h1>" + encode(title) + "</h1>\n"
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	76
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	77
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	78	/* common markup elements */
33984 c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	79
51402 b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	80	private def session_entry(entry: (String, String)): String =
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	81	{
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	82	val (name, description) = entry
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	83	val descr =
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	84	if (description == "") Nil
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	85	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	86	XML.string_of_tree(
5b2bf7611662 maintain session index on Scala side, for more determistic results; wenzelm parents: 50201 diff changeset	87	XML.elem("li",
5b2bf7611662 maintain session index on Scala side, for more determistic results; wenzelm parents: 50201 diff changeset	88	List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),
51402 b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	89	List(XML.Text(name)))) ::: descr)) + "\n"
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	90	}
34002 cbeeef3aebb3 basic treatment of special control symbols; wenzelm parents: 34000 diff changeset	91
51402 b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	92	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	93	{
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	94	begin_document("Isabelle/" + chapter + " sessions") +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	95	(if (sessions.isEmpty) ""
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	96	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	97	end_document
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	98	}
33984 c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	99	}

author	wenzelm
	Sat, 29 Nov 2014 14:43:10 +0100
changeset 59063	b3c45d0e4fe1
parent 56748	10b52ca3b4a2
child 60033	9a1d40876e9f
permissions	-rw-r--r--