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

author	wenzelm
	Wed, 13 Mar 2013 17:06:45 +0100
changeset 51420	9cf33e987f0b
parent 51402	b05cd411d3d3
child 54379	4fac53028f87
permissions	-rw-r--r--