isabelle: src/Pure/Thy/html.scala@7621a3b42ce7 (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	{
51399 6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	13	/* encode text */
37200 0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	14
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	15	def encode(text: String): String =
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	16	{
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	17	val s = new StringBuilder
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	18	for (c <- text.iterator) c match {
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	19	case '<' => s ++= "<"
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	20	case '>' => s ++= ">"
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	21	case '&' => s ++= "&"
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	22	case '"' => s ++= """
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	23	case '\'' => s ++= "'"
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	24	case '\n' => s ++= "<br/>"
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	25	case _ => s += c
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	26	}
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	27	s.toString
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	28	}
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	29
0f3edc64356a added HTML.encode (in Scala), similar to HTML.output in ML; wenzelm parents: 36016 diff changeset	30
51399 6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	31	/* document */
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	32
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	33	val end_document = "\n</div>\n</body>\n</html>\n"
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	34
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	35	def begin_document(title: String): String =
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	36	"<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	37	"<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	38	"\"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	39	"<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	40	"<head>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	41	"<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	42	"<title>" + encode(title) + "</title>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	43	"<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	44	"</head>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	45	"\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	46	"<body>\n" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	47	"<div class=\"head\">" +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	48	"<h1>" + encode(title) + "</h1>\n"
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	49
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	50
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	51	/* common markup elements */
33984 c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	52
51402 b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	53	private def session_entry(entry: (String, String)): String =
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	54	{
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	55	val (name, description) = entry
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	56	val descr =
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	57	if (description == "") Nil
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	58	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	59	XML.string_of_tree(
5b2bf7611662 maintain session index on Scala side, for more determistic results; wenzelm parents: 50201 diff changeset	60	XML.elem("li",
5b2bf7611662 maintain session index on Scala side, for more determistic results; wenzelm parents: 50201 diff changeset	61	List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),
51402 b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	62	List(XML.Text(name)))) ::: descr)) + "\n"
b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	63	}
34002 cbeeef3aebb3 basic treatment of special control symbols; wenzelm parents: 34000 diff changeset	64
51402 b05cd411d3d3 include session description in chapter index; wenzelm parents: 51399 diff changeset	65	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	66	{
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	67	begin_document("Isabelle/" + chapter + " sessions") +
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	68	(if (sessions.isEmpty) ""
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	69	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	70	end_document
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path); wenzelm parents: 50707 diff changeset	71	}
33984 c54498f88a77 Basic HTML output. wenzelm parents: diff changeset	72	}

author	paulson <lp15@cam.ac.uk>
	Fri, 27 Jun 2014 00:21:11 +0100
changeset 57394	7621a3b42ce7
parent 56748	10b52ca3b4a2
child 59063	b3c45d0e4fe1
permissions	-rw-r--r--