author | wenzelm |
Fri, 03 Dec 2010 21:30:41 +0100 | |
changeset 40946 | 3f697c636fa1 |
parent 39616 | 8052101883c3 |
child 41482 | f4c07fdd1d48 |
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 |
|
23724 | 9 |
val html_mode: ('a -> 'b) -> 'a -> 'b |
23622 | 10 |
type text = string |
6324 | 11 |
val plain: string -> text |
12 |
val name: string -> text |
|
13 |
val keyword: string -> text |
|
23622 | 14 |
val command: string -> text |
6324 | 15 |
val file_name: string -> text |
6649 | 16 |
val file_path: Url.T -> 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 |
6324 | 21 |
val preform: text -> text |
22 |
val verbatim: string -> text |
|
23724 | 23 |
val begin_document: string -> text |
24 |
val end_document: text |
|
17080 | 25 |
val begin_index: Url.T * string -> Url.T * string -> (Url.T * string) list -> Url.T -> text |
9415 | 26 |
val applet_pages: string -> Url.T * string -> (string * string) list |
6649 | 27 |
val theory_entry: Url.T * string -> text |
28 |
val session_entries: (Url.T * string) list -> text |
|
27861
911bf8e58c4c
removed obsolete verbatim_source, results, chapter, section etc.;
wenzelm
parents:
27832
diff
changeset
|
29 |
val theory_source: text -> text |
6649 | 30 |
val begin_theory: Url.T * string -> string -> (Url.T option * string) list -> |
27490 | 31 |
(Url.T * Url.T * bool) list -> text -> text |
37940
4857eab31298
generic external source files -- nothing special about ML here;
wenzelm
parents:
37146
diff
changeset
|
32 |
val external_file: Url.T -> string -> text |
6324 | 33 |
end; |
34 |
||
35 |
structure HTML: HTML = |
|
36 |
struct |
|
37 |
||
38 |
||
39 |
(** HTML print modes **) |
|
40 |
||
41 |
(* mode *) |
|
42 |
||
43 |
val htmlN = "HTML"; |
|
37146
f652333bbf8e
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
wenzelm
parents:
34003
diff
changeset
|
44 |
fun html_mode f x = Print_Mode.with_modes [htmlN] f x; |
6324 | 45 |
|
46 |
||
33985 | 47 |
(* common markup *) |
48 |
||
49 |
fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>"); |
|
50 |
||
51 |
val _ = Markup.add_mode htmlN (fn (name, _) => span name); |
|
52 |
||
53 |
||
6324 | 54 |
(* symbol output *) |
55 |
||
6338 | 56 |
local |
33985 | 57 |
val hidden = XML.text #> (span Markup.hiddenN |-> enclose); |
58 |
||
16196 | 59 |
val html_syms = Symtab.make |
34003
610e41138486
output_syms: permissive treatment of control symbols, cf. Scala version;
wenzelm
parents:
33986
diff
changeset
|
60 |
[("", (0, "")), |
610e41138486
output_syms: permissive treatment of control symbols, cf. Scala version;
wenzelm
parents:
33986
diff
changeset
|
61 |
("\n", (0, "<br/>")), |
33986
041dc6d8d344
output linefeed as </br> -- workaround problem with <pre> in Lobo Browser 0.98.4;
wenzelm
parents:
33985
diff
changeset
|
62 |
("'", (1, "'")), |
33983
cfbf1ff6170d
output "'" as "'" which is a bit more portable ("'" is defined in XML/XHTML, but not in old-style HTML4);
wenzelm
parents:
33222
diff
changeset
|
63 |
("\\<spacespace>", (2, " ")), |
23622 | 64 |
("\\<exclamdown>", (1, "¡")), |
65 |
("\\<cent>", (1, "¢")), |
|
66 |
("\\<pounds>", (1, "£")), |
|
67 |
("\\<currency>", (1, "¤")), |
|
68 |
("\\<yen>", (1, "¥")), |
|
69 |
("\\<bar>", (1, "¦")), |
|
70 |
("\\<section>", (1, "§")), |
|
71 |
("\\<dieresis>", (1, "¨")), |
|
72 |
("\\<copyright>", (1, "©")), |
|
73 |
("\\<ordfeminine>", (1, "ª")), |
|
74 |
("\\<guillemotleft>", (1, "«")), |
|
75 |
("\\<not>", (1, "¬")), |
|
76 |
("\\<hyphen>", (1, "­")), |
|
77 |
("\\<registered>", (1, "®")), |
|
78 |
("\\<inverse>", (1, "¯")), |
|
79 |
("\\<degree>", (1, "°")), |
|
80 |
("\\<plusminus>", (1, "±")), |
|
81 |
("\\<twosuperior>", (1, "²")), |
|
82 |
("\\<threesuperior>", (1, "³")), |
|
83 |
("\\<acute>", (1, "´")), |
|
84 |
("\\<paragraph>", (1, "¶")), |
|
85 |
("\\<cdot>", (1, "·")), |
|
86 |
("\\<cedilla>", (1, "¸")), |
|
87 |
("\\<onesuperior>", (1, "¹")), |
|
88 |
("\\<ordmasculine>", (1, "º")), |
|
89 |
("\\<guillemotright>", (1, "»")), |
|
90 |
("\\<onequarter>", (1, "¼")), |
|
91 |
("\\<onehalf>", (1, "½")), |
|
92 |
("\\<threequarters>", (1, "¾")), |
|
93 |
("\\<questiondown>", (1, "¿")), |
|
94 |
("\\<times>", (1, "×")), |
|
95 |
("\\<div>", (1, "÷")), |
|
96 |
("\\<circ>", (1, "o")), |
|
97 |
("\\<Alpha>", (1, "Α")), |
|
98 |
("\\<Beta>", (1, "Β")), |
|
99 |
("\\<Gamma>", (1, "Γ")), |
|
100 |
("\\<Delta>", (1, "Δ")), |
|
101 |
("\\<Epsilon>", (1, "Ε")), |
|
102 |
("\\<Zeta>", (1, "Ζ")), |
|
103 |
("\\<Eta>", (1, "Η")), |
|
104 |
("\\<Theta>", (1, "Θ")), |
|
105 |
("\\<Iota>", (1, "Ι")), |
|
106 |
("\\<Kappa>", (1, "Κ")), |
|
107 |
("\\<Lambda>", (1, "Λ")), |
|
108 |
("\\<Mu>", (1, "Μ")), |
|
109 |
("\\<Nu>", (1, "Ν")), |
|
110 |
("\\<Xi>", (1, "Ξ")), |
|
111 |
("\\<Omicron>", (1, "Ο")), |
|
112 |
("\\<Pi>", (1, "Π")), |
|
113 |
("\\<Rho>", (1, "Ρ")), |
|
114 |
("\\<Sigma>", (1, "Σ")), |
|
115 |
("\\<Tau>", (1, "Τ")), |
|
116 |
("\\<Upsilon>", (1, "Υ")), |
|
117 |
("\\<Phi>", (1, "Φ")), |
|
118 |
("\\<Chi>", (1, "Χ")), |
|
119 |
("\\<Psi>", (1, "Ψ")), |
|
120 |
("\\<Omega>", (1, "Ω")), |
|
121 |
("\\<alpha>", (1, "α")), |
|
122 |
("\\<beta>", (1, "β")), |
|
123 |
("\\<gamma>", (1, "γ")), |
|
124 |
("\\<delta>", (1, "δ")), |
|
125 |
("\\<epsilon>", (1, "ε")), |
|
126 |
("\\<zeta>", (1, "ζ")), |
|
127 |
("\\<eta>", (1, "η")), |
|
128 |
("\\<theta>", (1, "ϑ")), |
|
129 |
("\\<iota>", (1, "ι")), |
|
130 |
("\\<kappa>", (1, "κ")), |
|
131 |
("\\<lambda>", (1, "λ")), |
|
132 |
("\\<mu>", (1, "μ")), |
|
133 |
("\\<nu>", (1, "ν")), |
|
134 |
("\\<xi>", (1, "ξ")), |
|
135 |
("\\<omicron>", (1, "ο")), |
|
136 |
("\\<pi>", (1, "π")), |
|
137 |
("\\<rho>", (1, "ρ")), |
|
138 |
("\\<sigma>", (1, "σ")), |
|
139 |
("\\<tau>", (1, "τ")), |
|
140 |
("\\<upsilon>", (1, "υ")), |
|
141 |
("\\<phi>", (1, "φ")), |
|
142 |
("\\<chi>", (1, "χ")), |
|
143 |
("\\<psi>", (1, "ψ")), |
|
144 |
("\\<omega>", (1, "ω")), |
|
145 |
("\\<bullet>", (1, "•")), |
|
146 |
("\\<dots>", (1, "…")), |
|
147 |
("\\<Re>", (1, "ℜ")), |
|
148 |
("\\<Im>", (1, "ℑ")), |
|
149 |
("\\<wp>", (1, "℘")), |
|
150 |
("\\<forall>", (1, "∀")), |
|
151 |
("\\<partial>", (1, "∂")), |
|
152 |
("\\<exists>", (1, "∃")), |
|
153 |
("\\<emptyset>", (1, "∅")), |
|
154 |
("\\<nabla>", (1, "∇")), |
|
155 |
("\\<in>", (1, "∈")), |
|
156 |
("\\<notin>", (1, "∉")), |
|
157 |
("\\<Prod>", (1, "∏")), |
|
158 |
("\\<Sum>", (1, "∑")), |
|
159 |
("\\<star>", (1, "∗")), |
|
160 |
("\\<propto>", (1, "∝")), |
|
161 |
("\\<infinity>", (1, "∞")), |
|
162 |
("\\<angle>", (1, "∠")), |
|
163 |
("\\<and>", (1, "∧")), |
|
164 |
("\\<or>", (1, "∨")), |
|
165 |
("\\<inter>", (1, "∩")), |
|
166 |
("\\<union>", (1, "∪")), |
|
167 |
("\\<sim>", (1, "∼")), |
|
168 |
("\\<cong>", (1, "≅")), |
|
169 |
("\\<approx>", (1, "≈")), |
|
170 |
("\\<noteq>", (1, "≠")), |
|
171 |
("\\<equiv>", (1, "≡")), |
|
172 |
("\\<le>", (1, "≤")), |
|
173 |
("\\<ge>", (1, "≥")), |
|
174 |
("\\<subset>", (1, "⊂")), |
|
175 |
("\\<supset>", (1, "⊃")), |
|
176 |
("\\<subseteq>", (1, "⊆")), |
|
177 |
("\\<supseteq>", (1, "⊇")), |
|
178 |
("\\<oplus>", (1, "⊕")), |
|
179 |
("\\<otimes>", (1, "⊗")), |
|
180 |
("\\<bottom>", (1, "⊥")), |
|
181 |
("\\<lceil>", (1, "⌈")), |
|
182 |
("\\<rceil>", (1, "⌉")), |
|
183 |
("\\<lfloor>", (1, "⌊")), |
|
184 |
("\\<rfloor>", (1, "⌋")), |
|
185 |
("\\<langle>", (1, "⟨")), |
|
186 |
("\\<rangle>", (1, "⟩")), |
|
187 |
("\\<lozenge>", (1, "◊")), |
|
188 |
("\\<spadesuit>", (1, "♠")), |
|
189 |
("\\<clubsuit>", (1, "♣")), |
|
190 |
("\\<heartsuit>", (1, "♥")), |
|
191 |
("\\<diamondsuit>", (1, "♦")), |
|
192 |
("\\<lbrakk>", (2, "[|")), |
|
193 |
("\\<rbrakk>", (2, "|]")), |
|
194 |
("\\<Longrightarrow>", (3, "==>")), |
|
195 |
("\\<Rightarrow>", (2, "=>")), |
|
196 |
("\\<And>", (2, "!!")), |
|
197 |
("\\<Colon>", (2, "::")), |
|
198 |
("\\<lparr>", (2, "(|")), |
|
199 |
("\\<rparr>", (2, "|)),")), |
|
200 |
("\\<longleftrightarrow>", (3, "<->")), |
|
201 |
("\\<longrightarrow>", (3, "-->")), |
|
202 |
("\\<rightarrow>", (2, "->")), |
|
33985 | 203 |
("\\<^bsub>", (0, hidden "\\<^bsub>" ^ "<sub>")), |
204 |
("\\<^esub>", (0, hidden "\\<^esub>" ^ "</sub>")), |
|
205 |
("\\<^bsup>", (0, hidden "\\<^bsup>" ^ "<sup>")), |
|
206 |
("\\<^esup>", (0, hidden "\\<^esup>" ^ "</sup>"))]; |
|
17178 | 207 |
|
16196 | 208 |
fun output_sym s = |
23622 | 209 |
if Symbol.is_raw s then (1, Symbol.decode_raw s) |
20742 | 210 |
else |
33983
cfbf1ff6170d
output "'" as "'" which is a bit more portable ("'" is defined in XML/XHTML, but not in old-style HTML4);
wenzelm
parents:
33222
diff
changeset
|
211 |
(case Symtab.lookup html_syms s of |
cfbf1ff6170d
output "'" as "'" which is a bit more portable ("'" is defined in XML/XHTML, but not in old-style HTML4);
wenzelm
parents:
33222
diff
changeset
|
212 |
SOME x => x |
26709 | 213 |
| NONE => (size s, XML.text s)); |
6324 | 214 |
|
33985 | 215 |
fun output_markup (bg, en) s1 s2 = |
216 |
let val (n, txt) = output_sym s2 |
|
217 |
in (n, hidden s1 ^ enclose bg en txt) end; |
|
14534 | 218 |
|
33985 | 219 |
val output_sub = output_markup ("<sub>", "</sub>"); |
220 |
val output_sup = output_markup ("<sup>", "</sup>"); |
|
221 |
val output_bold = output_markup (span "bold"); |
|
222 |
val output_loc = output_markup (span "loc"); |
|
223 |
||
34003
610e41138486
output_syms: permissive treatment of control symbols, cf. Scala version;
wenzelm
parents:
33986
diff
changeset
|
224 |
fun output_syms (s1 :: rest) = |
610e41138486
output_syms: permissive treatment of control symbols, cf. Scala version;
wenzelm
parents:
33986
diff
changeset
|
225 |
let val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss)) in |
610e41138486
output_syms: permissive treatment of control symbols, cf. Scala version;
wenzelm
parents:
33986
diff
changeset
|
226 |
if s1 = "\\<^sub>" orelse s1 = "\\<^isub>" then output_sub s1 s2 :: output_syms ss |
610e41138486
output_syms: permissive treatment of control symbols, cf. Scala version;
wenzelm
parents:
33986
diff
changeset
|
227 |
else if s1 = "\\<^sup>" orelse s1 = "\\<^isup>" then output_sup s1 s2 :: output_syms ss |
610e41138486
output_syms: permissive treatment of control symbols, cf. Scala version;
wenzelm
parents:
33986
diff
changeset
|
228 |
else if s1 = "\\<^bold>" then output_bold s1 s2 :: output_syms ss |
610e41138486
output_syms: permissive treatment of control symbols, cf. Scala version;
wenzelm
parents:
33986
diff
changeset
|
229 |
else if s1 = "\\<^loc>" then output_loc s1 s2 :: output_syms ss |
610e41138486
output_syms: permissive treatment of control symbols, cf. Scala version;
wenzelm
parents:
33986
diff
changeset
|
230 |
else output_sym s1 :: output_syms rest |
610e41138486
output_syms: permissive treatment of control symbols, cf. Scala version;
wenzelm
parents:
33986
diff
changeset
|
231 |
end |
17178 | 232 |
| output_syms [] = []; |
6338 | 233 |
in |
6324 | 234 |
|
6338 | 235 |
fun output_width str = |
33986
041dc6d8d344
output linefeed as </br> -- workaround problem with <pre> in Lobo Browser 0.98.4;
wenzelm
parents:
33985
diff
changeset
|
236 |
let val (syms, width) = |
041dc6d8d344
output linefeed as </br> -- workaround problem with <pre> in Lobo Browser 0.98.4;
wenzelm
parents:
33985
diff
changeset
|
237 |
fold_map (fn (w, s) => fn width => (s, w + width)) (output_syms (Symbol.explode str)) 0 |
041dc6d8d344
output linefeed as </br> -- workaround problem with <pre> in Lobo Browser 0.98.4;
wenzelm
parents:
33985
diff
changeset
|
238 |
in (implode syms, width) end; |
6338 | 239 |
|
240 |
val output = #1 o output_width; |
|
241 |
||
26709 | 242 |
val _ = Output.add_mode htmlN output_width Symbol.encode_raw; |
243 |
||
6338 | 244 |
end; |
245 |
||
6324 | 246 |
|
247 |
||
248 |
(** HTML markup **) |
|
249 |
||
250 |
type text = string; |
|
251 |
||
252 |
||
253 |
(* atoms *) |
|
254 |
||
255 |
val plain = output; |
|
19265 | 256 |
val name = enclose "<span class=\"name\">" "</span>" o output; |
257 |
val keyword = enclose "<span class=\"keyword\">" "</span>" o output; |
|
23622 | 258 |
val command = enclose "<span class=\"command\">" "</span>" o output; |
19265 | 259 |
val file_name = enclose "<span class=\"filename\">" "</span>" o output; |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20742
diff
changeset
|
260 |
val file_path = file_name o Url.implode; |
6324 | 261 |
|
262 |
||
263 |
(* misc *) |
|
264 |
||
28840 | 265 |
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
|
266 |
fun href_path path txt = href_name (Url.implode path) txt; |
6376 | 267 |
|
15531 | 268 |
fun href_opt_path NONE txt = txt |
269 |
| href_opt_path (SOME p) txt = href_path p txt; |
|
6376 | 270 |
|
12413 | 271 |
fun para txt = "\n<p>" ^ txt ^ "</p>\n"; |
27830 | 272 |
fun preform txt = "<pre>" ^ txt ^ "</pre>"; |
6324 | 273 |
val verbatim = preform o output; |
274 |
||
275 |
||
276 |
(* document *) |
|
277 |
||
278 |
fun begin_document title = |
|
40946
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
279 |
"<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
280 |
\<!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
|
281 |
\\"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
|
282 |
\<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
283 |
\<head>\n\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
284 |
\<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
|
285 |
\<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
286 |
\<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
|
287 |
\</head>\n\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
288 |
\\n\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
289 |
\<body>\n\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
290 |
\<div class=\"head\">\ |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
39616
diff
changeset
|
291 |
\<h1>" ^ plain title ^ "</h1>\n"; |
6324 | 292 |
|
14541 | 293 |
val end_document = "\n</div>\n</body>\n</html>\n"; |
6324 | 294 |
|
6754 | 295 |
fun gen_link how (path, name) = para (href_path path how ^ " to index of " ^ plain name); |
296 |
val up_link = gen_link "Up"; |
|
297 |
val back_link = gen_link "Back"; |
|
6338 | 298 |
|
299 |
||
300 |
(* session index *) |
|
301 |
||
17080 | 302 |
fun begin_index up (index_path, session) docs graph = |
6754 | 303 |
begin_document ("Index of " ^ session) ^ up_link up ^ |
304 |
para ("View " ^ href_path graph "theory dependencies" ^ |
|
27829 | 305 |
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
|
306 |
"\n</div>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n"; |
6338 | 307 |
|
6649 | 308 |
fun choice chs s = space_implode " " (map (fn (s', lnk) => |
309 |
enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs); |
|
310 |
||
9415 | 311 |
fun applet_pages session back = |
6649 | 312 |
let |
9415 | 313 |
val sizes = |
314 |
[("small", "small.html", ("500", "400")), |
|
315 |
("medium", "medium.html", ("650", "520")), |
|
316 |
("large", "large.html", ("800", "640"))]; |
|
6649 | 317 |
|
9415 | 318 |
fun applet_page (size, name, (width, height)) = |
6754 | 319 |
let |
320 |
val browser_size = "Set browser size: " ^ |
|
9415 | 321 |
choice (map (fn (y, z, _) => (y, z)) sizes) size; |
6754 | 322 |
in |
323 |
(name, begin_document ("Theory dependencies of " ^ session) ^ |
|
324 |
back_link back ^ |
|
9415 | 325 |
para browser_size ^ |
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
|
326 |
"\n</div>\n<div class=\"graphbrowser\">\n\ |
17080 | 327 |
\<applet code=\"GraphBrowser/GraphBrowser.class\" \ |
14541 | 328 |
\archive=\"GraphBrowser.jar\" \ |
27832
992c6d984925
<applet>: more XHTML 1.0 Transitional conformance;
wenzelm
parents:
27830
diff
changeset
|
329 |
\width=" ^ quote width ^ " height=" ^ quote height ^ ">\n\ |
992c6d984925
<applet>: more XHTML 1.0 Transitional conformance;
wenzelm
parents:
27830
diff
changeset
|
330 |
\<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\"/>\n\ |
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
|
331 |
\</applet>" ^ end_document) |
6649 | 332 |
end; |
9415 | 333 |
in map applet_page sizes end; |
6649 | 334 |
|
335 |
||
27829 | 336 |
fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\n"; |
6405 | 337 |
|
6338 | 338 |
val theory_entry = entry; |
339 |
||
6405 | 340 |
fun session_entries [] = "</ul>" |
341 |
| session_entries es = |
|
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
|
342 |
"</ul>\n</div>\n<div class=\"sessions\">\n\ |
17080 | 343 |
\<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>"; |
6324 | 344 |
|
345 |
||
346 |
(* theory *) |
|
347 |
||
27861
911bf8e58c4c
removed obsolete verbatim_source, results, chapter, section etc.;
wenzelm
parents:
27832
diff
changeset
|
348 |
val theory_source = enclose |
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
|
349 |
"\n</div>\n<div class=\"source\">\n<pre>" |
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
|
350 |
"</pre>\n"; |
6324 | 351 |
|
352 |
||
353 |
local |
|
27490 | 354 |
fun file (href, path, loadit) = |
355 |
href_path href (if loadit then file_path path else enclose "(" ")" (file_path path)); |
|
6361 | 356 |
|
6376 | 357 |
fun theory up A = |
358 |
begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^ |
|
23622 | 359 |
command "theory" ^ " " ^ name A; |
16267
0773b17922d8
present new-style theory header, with 'imports' and 'uses';
wenzelm
parents:
16196
diff
changeset
|
360 |
|
0773b17922d8
present new-style theory header, with 'imports' and 'uses';
wenzelm
parents:
16196
diff
changeset
|
361 |
fun imports Bs = |
0773b17922d8
present new-style theory header, with 'imports' and 'uses';
wenzelm
parents:
16196
diff
changeset
|
362 |
keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs); |
0773b17922d8
present new-style theory header, with 'imports' and 'uses';
wenzelm
parents:
16196
diff
changeset
|
363 |
|
27829 | 364 |
fun uses Ps = keyword "uses" ^ " " ^ space_implode " " (map file Ps) ^ "<br/>\n"; |
6324 | 365 |
in |
366 |
||
16267
0773b17922d8
present new-style theory header, with 'imports' and 'uses';
wenzelm
parents:
16196
diff
changeset
|
367 |
fun begin_theory up A Bs Ps body = |
27829 | 368 |
theory up A ^ "<br/>\n" ^ |
369 |
imports Bs ^ "<br/>\n" ^ |
|
16267
0773b17922d8
present new-style theory header, with 'imports' and 'uses';
wenzelm
parents:
16196
diff
changeset
|
370 |
(if null Ps then "" else uses Ps) ^ |
0773b17922d8
present new-style theory header, with 'imports' and 'uses';
wenzelm
parents:
16196
diff
changeset
|
371 |
body; |
0773b17922d8
present new-style theory header, with 'imports' and 'uses';
wenzelm
parents:
16196
diff
changeset
|
372 |
|
6324 | 373 |
end; |
374 |
||
375 |
||
37940
4857eab31298
generic external source files -- nothing special about ML here;
wenzelm
parents:
37146
diff
changeset
|
376 |
(* external file *) |
6324 | 377 |
|
37940
4857eab31298
generic external source files -- nothing special about ML here;
wenzelm
parents:
37146
diff
changeset
|
378 |
fun external_file path str = |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20742
diff
changeset
|
379 |
begin_document ("File " ^ Url.implode path) ^ |
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
|
380 |
"\n</div><div class=\"external_source\">\n" ^ |
14571 | 381 |
verbatim str ^ |
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
|
382 |
"\n</div>\n<div class=\"external_footer\">" ^ |
14541 | 383 |
end_document; |
6324 | 384 |
|
7572 | 385 |
end; |