author | wenzelm |
Fri, 09 Oct 2015 21:16:00 +0200 | |
changeset 61379 | c57820ceead3 |
parent 61376 | 93224745477f |
child 61381 | ddca85598c65 |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: Pure/Thy/html.ML |
9415 | 2 |
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen |
6324 | 3 |
|
9415 | 4 |
HTML presentation elements. |
6324 | 5 |
*) |
6 |
||
7 |
signature HTML = |
|
8 |
sig |
|
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
9 |
val reset_symbols: unit -> unit |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
10 |
val init_symbols: (string * int) list -> unit |
61379
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
11 |
val present_span: Keyword.keywords -> Command_Span.span -> Output.output |
23622 | 12 |
type text = string |
6324 | 13 |
val plain: string -> text |
14 |
val name: string -> text |
|
15 |
val keyword: string -> text |
|
23622 | 16 |
val command: string -> text |
6324 | 17 |
val href_name: string -> text -> text |
6649 | 18 |
val href_path: Url.T -> text -> text |
19 |
val href_opt_path: Url.T option -> text -> text |
|
6376 | 20 |
val para: text -> text |
23724 | 21 |
val begin_document: string -> text |
22 |
val end_document: text |
|
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
55041
diff
changeset
|
23 |
val begin_session_index: string -> Url.T -> (Url.T * string) list -> text |
6649 | 24 |
val theory_entry: Url.T * string -> text |
54456 | 25 |
val theory: string -> (Url.T option * string) list -> text -> text |
6324 | 26 |
end; |
27 |
||
28 |
structure HTML: HTML = |
|
29 |
struct |
|
30 |
||
31 |
||
33985 | 32 |
(* common markup *) |
33 |
||
34 |
fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>"); |
|
35 |
||
61379
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
36 |
val hidden = span Markup.hiddenN |-> enclose; |
33985 | 37 |
|
38 |
||
6324 | 39 |
(* symbol output *) |
40 |
||
6338 | 41 |
local |
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
42 |
|
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
43 |
val symbols = |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
44 |
Synchronized.var "HTML.symbols" (NONE: (int * string) Symtab.table option); |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
45 |
|
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
46 |
fun output_sym s = |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
47 |
if Symbol.is_raw s then (1, Symbol.decode_raw s) |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
48 |
else |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
49 |
(case Synchronized.value symbols of |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
50 |
SOME tab => |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
51 |
(case Symtab.lookup tab s of |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
52 |
SOME x => x |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
53 |
| NONE => (size s, XML.text s)) |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
54 |
| NONE => raise Fail "Missing HTML.init_symbols: cannot output symbols"); |
33985 | 55 |
|
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
56 |
fun output_markup (bg, en) s1 s2 = |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
57 |
let val (n, txt) = output_sym s2 |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
58 |
in (n, hidden s1 ^ enclose bg en txt) end; |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
59 |
|
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
60 |
val output_sub = output_markup ("<sub>", "</sub>"); |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
61 |
val output_sup = output_markup ("<sup>", "</sup>"); |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
62 |
val output_bold = output_markup (span "bold"); |
17178 | 63 |
|
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
64 |
fun output_syms [] (result, width) = (implode (rev result), width) |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
65 |
| output_syms (s1 :: rest) (result, width) = |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
66 |
let |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
67 |
val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss)); |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
68 |
val ((w, s), r) = |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
69 |
if s1 = "\\<^sub>" then (output_sub "⇩" s2, ss) |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
70 |
else if s1 = "\\<^sup>" then (output_sup "⇧" s2, ss) |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
71 |
else if s1 = "\\<^bold>" then (output_bold "❙" s2, ss) |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
72 |
else (output_sym s1, rest); |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
73 |
in output_syms r (s :: result, width + w) end; |
14534 | 74 |
|
6338 | 75 |
in |
6324 | 76 |
|
41482 | 77 |
fun output_width str = output_syms (Symbol.explode str) ([], 0); |
6338 | 78 |
val output = #1 o output_width; |
79 |
||
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
80 |
fun reset_symbols () = Synchronized.change symbols (K NONE); |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
81 |
|
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
82 |
fun init_symbols codes = |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
83 |
let |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
84 |
val mapping = |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
85 |
map (fn (s, c) => (s, (Symbol.length [s], "&#" ^ Markup.print_int c ^ ";"))) codes @ |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
86 |
[("", (0, "")), |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
87 |
("'", (1, "'")), |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
88 |
("\\<^bsub>", (0, hidden "⇘" ^ "<sub>")), |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
89 |
("\\<^esub>", (0, hidden "⇙" ^ "</sub>")), |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
90 |
("\\<^bsup>", (0, hidden "⇗" ^ "<sup>")), |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
91 |
("\\<^esup>", (0, hidden "⇖" ^ "</sup>"))]; |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
92 |
in Synchronized.change symbols (K (SOME (fold Symtab.update mapping Symtab.empty))) end; |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
61374
diff
changeset
|
93 |
|
6338 | 94 |
end; |
95 |
||
6324 | 96 |
|
61379
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
97 |
(* presentation *) |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
98 |
|
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
99 |
fun present_token keywords tok = |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
100 |
fold_rev (uncurry enclose o span o #1) |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
101 |
(Token.markups keywords tok) (output (Token.unparse tok)); |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
102 |
|
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
103 |
fun present_span keywords = |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
104 |
implode o map (present_token keywords) o Command_Span.content; |
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
105 |
|
c57820ceead3
more direct HTML presentation, without print mode;
wenzelm
parents:
61376
diff
changeset
|
106 |
|
6324 | 107 |
|
108 |
(** HTML markup **) |
|
109 |
||
110 |
type text = string; |
|
111 |
||
112 |
||
113 |
(* atoms *) |
|
114 |
||
115 |
val plain = output; |
|
19265 | 116 |
val name = enclose "<span class=\"name\">" "</span>" o output; |
117 |
val keyword = enclose "<span class=\"keyword\">" "</span>" o output; |
|
23622 | 118 |
val command = enclose "<span class=\"command\">" "</span>" o output; |
6324 | 119 |
|
120 |
||
121 |
(* misc *) |
|
122 |
||
28840 | 123 |
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
|
124 |
fun href_path path txt = href_name (Url.implode path) txt; |
6376 | 125 |
|
15531 | 126 |
fun href_opt_path NONE txt = txt |
127 |
| href_opt_path (SOME p) txt = href_path p txt; |
|
6376 | 128 |
|
12413 | 129 |
fun para txt = "\n<p>" ^ txt ^ "</p>\n"; |
6324 | 130 |
|
131 |
||
132 |
(* document *) |
|
133 |
||
134 |
fun begin_document title = |
|
40946
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
135 |
"<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
136 |
\<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
137 |
\\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
138 |
\<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
139 |
\<head>\n\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
140 |
\<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
141 |
\<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
142 |
\<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
143 |
\</head>\n\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
144 |
\\n\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
145 |
\<body>\n\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
146 |
\<div class=\"head\">\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
147 |
\<h1>" ^ plain title ^ "</h1>\n"; |
6324 | 148 |
|
14541 | 149 |
val end_document = "\n</div>\n</body>\n</html>\n"; |
6324 | 150 |
|
6338 | 151 |
|
152 |
(* session index *) |
|
153 |
||
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
55041
diff
changeset
|
154 |
fun begin_session_index session graph docs = |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50233
diff
changeset
|
155 |
begin_document ("Session " ^ plain session) ^ |
6754 | 156 |
para ("View " ^ href_path graph "theory dependencies" ^ |
27829 | 157 |
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
|
158 |
"\n</div>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n"; |
6338 | 159 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
50233
diff
changeset
|
160 |
fun theory_entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\n"; |
6324 | 161 |
|
162 |
||
163 |
(* theory *) |
|
164 |
||
54456 | 165 |
fun theory A Bs txt = |
166 |
begin_document ("Theory " ^ A) ^ "\n" ^ |
|
167 |
command "theory" ^ " " ^ name A ^ "<br/>\n" ^ |
|
54455
1d977436c1bf
removed remains of HTML presentation of auxiliary files -- inactive since Isabelle2013;
wenzelm
parents:
53194
diff
changeset
|
168 |
keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs) ^ |
54456 | 169 |
"<br/>\n" ^ |
61374 | 170 |
enclose "\n</div>\n<div class=\"source\">\n<pre class=\"source\">" "</pre>\n" txt ^ |
54456 | 171 |
end_document; |
16267
0773b17922d8
present new-style theory header, with 'imports' and 'uses';
wenzelm
parents:
16196
diff
changeset
|
172 |
|
6324 | 173 |
end; |