isabelle: src/Pure/Thy/html.ML@e98988801fa9 (annotated)

24584 01e83ffa6c54 fixed title haftmann parents: 24244 diff changeset	1	(* Title: Pure/Thy/html.ML
9415 daa2296f23ea removed all_sessions; wenzelm parents: 9045 diff changeset	2	Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	3
9415 daa2296f23ea removed all_sessions; wenzelm parents: 9045 diff changeset	4	HTML presentation elements.
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	5	*)
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	6
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	7	signature HTML =
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	8	sig
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	9	type symbols
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	10	val make_symbols: (string * int) list -> symbols
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	11	val no_symbols: symbols
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	12	val present_span: symbols -> Keyword.keywords -> Command_Span.span -> Output.output
23622 8ce09f692653 simplified pretty token metric: type int; wenzelm parents: 22796 diff changeset	13	type text = string
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	14	val begin_document: symbols -> string -> text
23724 6e95ed5f64da export html_mode, begin_document, end_document; wenzelm parents: 23703 diff changeset	15	val end_document: text
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	16	val begin_session_index: symbols -> string -> Url.T -> (Url.T * string) list -> text
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	17	val theory_entry: symbols -> Url.T * string -> text
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	18	val theory: symbols -> string -> (Url.T option * string) list -> text -> text
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	19	end;
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	20
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	21	structure HTML: HTML =
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	22	struct
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	23
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	24
33985 1d33e85a3fa9 added markup for hidden text; wenzelm parents: 33983 diff changeset	25	(* common markup *)
1d33e85a3fa9 added markup for hidden text; wenzelm parents: 33983 diff changeset	26
67306 897344e33c26 less redundant; wenzelm parents: 66044 diff changeset	27	fun span "" = ("<span>", "</span>")
897344e33c26 less redundant; wenzelm parents: 66044 diff changeset	28	\| span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
897344e33c26 less redundant; wenzelm parents: 66044 diff changeset	29
66044 bd7516709051 more HTML rendering as in Isabelle/jEdit; wenzelm parents: 63934 diff changeset	30	val enclose_span = uncurry enclose o span;
33985 1d33e85a3fa9 added markup for hidden text; wenzelm parents: 33983 diff changeset	31
66044 bd7516709051 more HTML rendering as in Isabelle/jEdit; wenzelm parents: 63934 diff changeset	32	val hidden = enclose_span Markup.hiddenN;
33985 1d33e85a3fa9 added markup for hidden text; wenzelm parents: 33983 diff changeset	33
1d33e85a3fa9 added markup for hidden text; wenzelm parents: 33983 diff changeset	34
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	35	(* symbol output *)
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	36
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	37	abstype symbols = Symbols of string Symtab.table
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	38	with
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	39
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	40	fun make_symbols codes =
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	41	let
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	42	val mapping =
63806 c54a53ef1873 clarified modules; wenzelm parents: 62529 diff changeset	43	map (apsnd (fn c => "&#" ^ Value.print_int c ^ ";")) codes @
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	44	[("'", "'"),
62529 8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	45	("\<^bsub>", hidden "⇘" ^ "<sub>"),
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	46	("\<^esub>", hidden "⇙" ^ "</sub>"),
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	47	("\<^bsup>", hidden "⇗" ^ "<sup>"),
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	48	("\<^esup>", hidden "⇖" ^ "</sup>")];
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	49	in Symbols (fold Symtab.update mapping Symtab.empty) end;
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	50
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	51	val no_symbols = make_symbols [];
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	52
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	53	fun output_sym (Symbols tab) s =
63934 397b25cee74c \<^raw> output is intended for LaTeX; wenzelm parents: 63806 diff changeset	54	(case Symtab.lookup tab s of
397b25cee74c \<^raw> output is intended for LaTeX; wenzelm parents: 63806 diff changeset	55	SOME x => x
397b25cee74c \<^raw> output is intended for LaTeX; wenzelm parents: 63806 diff changeset	56	\| NONE => XML.text s);
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	57
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	58	end;
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	59
6338 bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	60	local
61376 93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	61
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	62	fun output_markup (bg, en) symbols s1 s2 =
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	63	hidden s1 ^ enclose bg en (output_sym symbols s2);
61376 93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	64
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	65	val output_sub = output_markup ("<sub>", "</sub>");
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	66	val output_sup = output_markup ("<sup>", "</sup>");
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	67	val output_bold = output_markup (span "bold");
17178 18a98ecc6821 output \<^loc> as 'loc' span; wenzelm parents: 17116 diff changeset	68
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	69	fun output_syms _ [] result = implode (rev result)
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	70	\| output_syms symbols (s1 :: rest) result =
61376 93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	71	let
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	72	val (s2, ss) = (case rest of [] => ("", []) \| s2 :: ss => (s2, ss));
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	73	val (s, r) =
62529 8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	74	if s1 = "\<^sub>" then (output_sub symbols "⇩" s2, ss)
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	75	else if s1 = "\<^sup>" then (output_sup symbols "⇧" s2, ss)
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	76	else if s1 = "\<^bold>" then (output_bold symbols "❙" s2, ss)
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	77	else (output_sym symbols s1, rest);
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	78	in output_syms symbols r (s :: result) end;
14534 7a46bdcd92f2 treat sub/super scripts kleing parents: 14083 diff changeset	79
6338 bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	80	in
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	81
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	82	fun output symbols str = output_syms symbols (Symbol.explode str) [];
61376 93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation; wenzelm parents: 61374 diff changeset	83
6338 bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	84	end;
bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	85
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	86
61379 c57820ceead3 more direct HTML presentation, without print mode; wenzelm parents: 61376 diff changeset	87	(* presentation *)
c57820ceead3 more direct HTML presentation, without print mode; wenzelm parents: 61376 diff changeset	88
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	89	fun present_span symbols keywords =
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	90	let
66044 bd7516709051 more HTML rendering as in Isabelle/jEdit; wenzelm parents: 63934 diff changeset	91	fun present_markup (name, props) =
bd7516709051 more HTML rendering as in Isabelle/jEdit; wenzelm parents: 63934 diff changeset	92	(case Properties.get props Markup.kindN of
bd7516709051 more HTML rendering as in Isabelle/jEdit; wenzelm parents: 63934 diff changeset	93	SOME kind =>
bd7516709051 more HTML rendering as in Isabelle/jEdit; wenzelm parents: 63934 diff changeset	94	if kind = Markup.commandN orelse kind = Markup.keywordN then enclose_span kind else I
bd7516709051 more HTML rendering as in Isabelle/jEdit; wenzelm parents: 63934 diff changeset	95	\| NONE => I) #> enclose_span name;
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	96	fun present_token tok =
66044 bd7516709051 more HTML rendering as in Isabelle/jEdit; wenzelm parents: 63934 diff changeset	97	fold_rev present_markup (Token.markups keywords tok)
bd7516709051 more HTML rendering as in Isabelle/jEdit; wenzelm parents: 63934 diff changeset	98	(output symbols (Token.unparse tok));
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	99	in implode o map present_token o Command_Span.content end;
61379 c57820ceead3 more direct HTML presentation, without print mode; wenzelm parents: 61376 diff changeset	100
c57820ceead3 more direct HTML presentation, without print mode; wenzelm parents: 61376 diff changeset	101
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	102
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	103	( HTML markup )
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	104
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	105	type text = string;
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	106
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	107
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	108	(* atoms *)
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	109
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	110	val name = enclose "<span class=\"name\">" "</span>" oo output;
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	111	val keyword = enclose "<span class=\"keyword\">" "</span>" oo output;
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	112	val command = enclose "<span class=\"command\">" "</span>" oo output;
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	113
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	114
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	115	(* misc *)
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	116
28840 049f0a8faa35 tuned; wenzelm parents: 27896 diff changeset	117	fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
21858 05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert; wenzelm parents: 20742 diff changeset	118	fun href_path path txt = href_name (Url.implode path) txt;
6376 c87f3769203a tuned; wenzelm parents: 6361 diff changeset	119
15531 08c8dad8e399 Deleted Library.option type. skalberg parents: 15336 diff changeset	120	fun href_opt_path NONE txt = txt
08c8dad8e399 Deleted Library.option type. skalberg parents: 15336 diff changeset	121	\| href_opt_path (SOME p) txt = href_path p txt;
6376 c87f3769203a tuned; wenzelm parents: 6361 diff changeset	122
12413 f879fcc9412d tuned line breaks in HTML source; wenzelm parents: 12151 diff changeset	123	fun para txt = "\n<p>" ^ txt ^ "</p>\n";
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	124
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	125
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	126	(* document *)
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	127
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	128	fun begin_document symbols title =
62529 8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	129	"<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	130	"<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	131	"\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	132	"<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	133	"<head>\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	134	"<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	135	"<title>" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	136	"<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	137	"</head>\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	138	"\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	139	"<body>\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	140	"<div class=\"head\">" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap; wenzelm parents: 61381 diff changeset	141	"<h1>" ^ output symbols title ^ "</h1>\n";
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	142
14541 0a7743e2f8dd use css kleing parents: 14534 diff changeset	143	val end_document = "\n</div>\n</body>\n</html>\n";
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	144
6338 bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	145
bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	146	(* session index *)
bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	147
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	148	fun begin_session_index symbols session graph docs =
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	149	begin_document symbols ("Session " ^ output symbols session) ^
6754 c23c542a32e5 tuned markup; wenzelm parents: 6649 diff changeset	150	para ("View " ^ href_path graph "theory dependencies" ^
27829 c073006e0137 produce XHTML 1.0 Transitional; wenzelm parents: 27490 diff changeset	151	implode (map (fn (p, name) => "<br/>\nView " ^ href_path p name) docs)) ^
37941 1d812ff95a14 refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well; wenzelm parents: 37940 diff changeset	152	"\n</div>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
6338 bf0d22535e47 output: some symbol translations; wenzelm parents: 6324 diff changeset	153
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	154	fun theory_entry symbols (p, s) = "<li>" ^ href_path p (output symbols s) ^ "</li>\n";
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	155
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	156
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	157	(* theory *)
3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	158
61381 ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	159	fun theory symbols A Bs txt =
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	160	begin_document symbols ("Theory " ^ A) ^ "\n" ^
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	161	command symbols "theory" ^ " " ^ name symbols A ^ "<br/>\n" ^
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	162	keyword symbols "imports" ^ " " ^
ddca85598c65 more explicit HTML.symbols; wenzelm parents: 61379 diff changeset	163	space_implode " " (map (uncurry href_opt_path o apsnd (name symbols)) Bs) ^
54456 f4b1440d9880 simplified HTML theory presentation; wenzelm parents: 54455 diff changeset	164	"<br/>\n" ^
61374 b3c665940d62 server-side fonts; wenzelm parents: 59448 diff changeset	165	enclose "\n</div>\n<div class=\"source\">\n<pre class=\"source\">" "</pre>\n" txt ^
54456 f4b1440d9880 simplified HTML theory presentation; wenzelm parents: 54455 diff changeset	166	end_document;
16267 0773b17922d8 present new-style theory header, with 'imports' and 'uses'; wenzelm parents: 16196 diff changeset	167
6324 3b7111b360b1 HTML markup elements. wenzelm parents: diff changeset	168	end;

author	paulson <lp15@cam.ac.uk>
	Fri, 27 Apr 2018 20:59:34 +0100
changeset 68052	e98988801fa9
parent 67306	897344e33c26
child 69804	9efccbad7d42
permissions	-rw-r--r--