author | kleing |
Mon, 29 Nov 2004 06:09:45 +0100 | |
changeset 15336 | cb35ae957c65 |
parent 14992 | a16bc5abad45 |
child 15531 | 08c8dad8e399 |
permissions | -rw-r--r-- |
6324 | 1 |
(* Title: Pure/Thy/HTML.ML |
2 |
ID: $Id$ |
|
9415 | 3 |
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen |
6324 | 4 |
|
9415 | 5 |
HTML presentation elements. |
6324 | 6 |
*) |
7 |
||
8 |
signature HTML = |
|
9 |
sig |
|
10 |
val output: string -> string |
|
11 |
val output_width: string -> string * real |
|
12 |
type text (* = string *) |
|
13 |
val plain: string -> text |
|
14 |
val name: string -> text |
|
15 |
val keyword: string -> text |
|
16 |
val file_name: string -> text |
|
6649 | 17 |
val file_path: Url.T -> text |
6324 | 18 |
val href_name: string -> text -> text |
6649 | 19 |
val href_path: Url.T -> text -> text |
6376 | 20 |
val href_opt_name: string option -> text -> text |
6649 | 21 |
val href_opt_path: Url.T option -> text -> text |
6376 | 22 |
val para: text -> text |
6324 | 23 |
val preform: text -> text |
24 |
val verbatim: string -> text |
|
7725 | 25 |
val begin_index: Url.T * string -> Url.T * string -> Url.T option |
26 |
-> Url.T option -> Url.T -> text |
|
6338 | 27 |
val end_index: text |
9415 | 28 |
val applet_pages: string -> Url.T * string -> (string * string) list |
6649 | 29 |
val theory_entry: Url.T * string -> text |
30 |
val session_entries: (Url.T * string) list -> text |
|
8190 | 31 |
val verbatim_source: Symbol.symbol list -> text |
6649 | 32 |
val begin_theory: Url.T * string -> string -> (Url.T option * string) list -> |
7408 | 33 |
(Url.T option * Url.T * bool option) list -> text -> text |
6324 | 34 |
val end_theory: text |
6649 | 35 |
val ml_file: Url.T -> string -> text |
13531 | 36 |
val results: string -> (string * thm list) list -> text |
8088 | 37 |
val chapter: string -> text |
6324 | 38 |
val section: string -> text |
7634 | 39 |
val subsection: string -> text |
40 |
val subsubsection: string -> text |
|
6324 | 41 |
val setup: (theory -> theory) list |
42 |
end; |
|
43 |
||
44 |
structure HTML: HTML = |
|
45 |
struct |
|
46 |
||
47 |
||
48 |
(** HTML print modes **) |
|
49 |
||
50 |
(* mode *) |
|
51 |
||
52 |
val htmlN = "HTML"; |
|
10573 | 53 |
fun html_mode f x = setmp print_mode (htmlN :: ! print_mode) f x; |
6324 | 54 |
|
55 |
||
56 |
(* symbol output *) |
|
57 |
||
6338 | 58 |
local |
59 |
val escape = fn "<" => "<" | ">" => ">" | "&" => "&" | c => c; |
|
6324 | 60 |
|
6338 | 61 |
val output_sym = |
9963 | 62 |
fn "\\<spacespace>" => (2.0, " ") |
63 |
| "\\<exclamdown>" => (1.0, "¡") |
|
64 |
| "\\<cent>" => (1.0, "¢") |
|
65 |
| "\\<pounds>" => (1.0, "£") |
|
66 |
| "\\<currency>" => (1.0, "¤") |
|
67 |
| "\\<yen>" => (1.0, "¥") |
|
68 |
| "\\<bar>" => (1.0, "¦") |
|
69 |
| "\\<section>" => (1.0, "§") |
|
10837
7d640de604e4
added \<dieresis>, \<acute>, \<cedilla>, \<emptyset>;
wenzelm
parents:
10831
diff
changeset
|
70 |
| "\\<dieresis>" => (1.0, "¨") |
9963 | 71 |
| "\\<copyright>" => (1.0, "©") |
72 |
| "\\<ordfeminine>" => (1.0, "ª") |
|
73 |
| "\\<guillemotleft>" => (1.0, "«") |
|
74 |
| "\\<not>" => (1.0, "¬") |
|
6338 | 75 |
| "\\<hyphen>" => (1.0, "­") |
9963 | 76 |
| "\\<registered>" => (1.0, "®") |
10831 | 77 |
| "\\<inverse>" => (1.0, "¯") |
9963 | 78 |
| "\\<degree>" => (1.0, "°") |
79 |
| "\\<plusminus>" => (1.0, "±") |
|
80 |
| "\\<twosuperior>" => (1.0, "²") |
|
81 |
| "\\<threesuperior>" => (1.0, "³") |
|
10837
7d640de604e4
added \<dieresis>, \<acute>, \<cedilla>, \<emptyset>;
wenzelm
parents:
10831
diff
changeset
|
82 |
| "\\<acute>" => (1.0, "´") |
9963 | 83 |
| "\\<paragraph>" => (1.0, "¶") |
6338 | 84 |
| "\\<cdot>" => (1.0, "·") |
10837
7d640de604e4
added \<dieresis>, \<acute>, \<cedilla>, \<emptyset>;
wenzelm
parents:
10831
diff
changeset
|
85 |
| "\\<cedilla>" => (1.0, "¸") |
9963 | 86 |
| "\\<onesuperior>" => (1.0, "¹") |
87 |
| "\\<ordmasculine>" => (1.0, "º") |
|
88 |
| "\\<guillemotright>" => (1.0, "»") |
|
89 |
| "\\<onequarter>" => (1.0, "¼") |
|
90 |
| "\\<onehalf>" => (1.0, "½") |
|
91 |
| "\\<threequarters>" => (1.0, "¾") |
|
92 |
| "\\<questiondown>" => (1.0, "¿") |
|
6338 | 93 |
| "\\<times>" => (1.0, "×") |
9963 | 94 |
| "\\<div>" => (1.0, "÷") |
15336 | 95 |
| "\\<circ>" => (1.0, "o") |
14552 | 96 |
| "\\<Alpha>" => (1.0, "Α") |
97 |
| "\\<Beta>" => (1.0, "Β") |
|
98 |
| "\\<Gamma>" => (1.0, "Γ") |
|
99 |
| "\\<Delta>" => (1.0, "Δ") |
|
100 |
| "\\<Epsilon>" => (1.0, "Ε") |
|
101 |
| "\\<Zeta>" => (1.0, "Ζ") |
|
102 |
| "\\<Eta>" => (1.0, "Η") |
|
103 |
| "\\<Theta>" => (1.0, "Θ") |
|
104 |
| "\\<Iota>" => (1.0, "Ι") |
|
105 |
| "\\<Kappa>" => (1.0, "Κ") |
|
106 |
| "\\<Lambda>" => (1.0, "Λ") |
|
107 |
| "\\<Mu>" => (1.0, "Μ") |
|
108 |
| "\\<Nu>" => (1.0, "Ν") |
|
109 |
| "\\<Xi>" => (1.0, "Ξ") |
|
110 |
| "\\<Omicron>" => (1.0, "Ο") |
|
111 |
| "\\<Pi>" => (1.0, "Π") |
|
112 |
| "\\<Rho>" => (1.0, "Ρ") |
|
113 |
| "\\<Sigma>" => (1.0, "Σ") |
|
114 |
| "\\<Tau>" => (1.0, "Τ") |
|
115 |
| "\\<Upsilon>" => (1.0, "Υ") |
|
116 |
| "\\<Phi>" => (1.0, "Φ") |
|
117 |
| "\\<Chi>" => (1.0, "Χ") |
|
118 |
| "\\<Psi>" => (1.0, "Ψ") |
|
119 |
| "\\<Omega>" => (1.0, "Ω") |
|
120 |
| "\\<alpha>" => (1.0, "α") |
|
121 |
| "\\<beta>" => (1.0, "β") |
|
122 |
| "\\<gamma>" => (1.0, "γ") |
|
123 |
| "\\<delta>" => (1.0, "δ") |
|
124 |
| "\\<epsilon>" => (1.0, "ε") |
|
125 |
| "\\<zeta>" => (1.0, "ζ") |
|
126 |
| "\\<eta>" => (1.0, "η") |
|
127 |
| "\\<theta>" => (1.0, "ϑ") |
|
128 |
| "\\<iota>" => (1.0, "ι") |
|
129 |
| "\\<kappa>" => (1.0, "κ") |
|
130 |
| "\\<lambda>" => (1.0, "λ") |
|
131 |
| "\\<mu>" => (1.0, "μ") |
|
132 |
| "\\<nu>" => (1.0, "ν") |
|
133 |
| "\\<xi>" => (1.0, "ξ") |
|
134 |
| "\\<omicron>" => (1.0, "ο") |
|
135 |
| "\\<pi>" => (1.0, "π") |
|
136 |
| "\\<rho>" => (1.0, "ρ") |
|
137 |
| "\\<sigma>" => (1.0, "σ") |
|
138 |
| "\\<tau>" => (1.0, "τ") |
|
139 |
| "\\<upsilon>" => (1.0, "υ") |
|
140 |
| "\\<phi>" => (1.0, "φ") |
|
141 |
| "\\<chi>" => (1.0, "χ") |
|
142 |
| "\\<psi>" => (1.0, "ψ") |
|
143 |
| "\\<omega>" => (1.0, "ω") |
|
144 |
| "\\<buller>" => (1.0, "•") |
|
145 |
| "\\<dots>" => (1.0, "…") |
|
146 |
| "\\<Re>" => (1.0, "ℜ") |
|
147 |
| "\\<Im>" => (1.0, "ℑ") |
|
148 |
| "\\<wp>" => (1.0, "℘") |
|
149 |
| "\\<forall>" => (1.0, "∀") |
|
150 |
| "\\<partial>" => (1.0, "∂") |
|
151 |
| "\\<exists>" => (1.0, "∃") |
|
152 |
| "\\<emptyset>" => (1.0, "∅") |
|
153 |
| "\\<nabla>" => (1.0, "∇") |
|
154 |
| "\\<in>" => (1.0, "∈") |
|
155 |
| "\\<notin>" => (1.0, "∉") |
|
14565 | 156 |
| "\\<Prod>" => (1.0, "∏") |
157 |
| "\\<Sum>" => (1.0, "∑") |
|
14552 | 158 |
| "\\<star>" => (1.0, "∗") |
159 |
| "\\<propto>" => (1.0, "∝") |
|
160 |
| "\\<infinity>" => (1.0, "∞") |
|
161 |
| "\\<angle>" => (1.0, "∠") |
|
14571 | 162 |
| "\\<and>" => (1.0, "∧") |
14552 | 163 |
| "\\<or>" => (1.0, "∨") |
164 |
| "\\<inter>" => (1.0, "∩") |
|
165 |
| "\\<union>" => (1.0, "∪") |
|
166 |
| "\\<sim>" => (1.0, "∼") |
|
167 |
| "\\<cong>" => (1.0, "≅") |
|
168 |
| "\\<approx>" => (1.0, "≈") |
|
169 |
| "\\<noteq>" => (1.0, "≠") |
|
170 |
| "\\<equiv>" => (1.0, "≡") |
|
171 |
| "\\<le>" => (1.0, "≤") |
|
172 |
| "\\<ge>" => (1.0, "≥") |
|
173 |
| "\\<subset>" => (1.0, "⊂") |
|
174 |
| "\\<supset>" => (1.0, "⊃") |
|
175 |
| "\\<subseteq>" => (1.0, "⊆") |
|
176 |
| "\\<supseteq>" => (1.0, "⊇") |
|
177 |
| "\\<oplus>" => (1.0, "⊕") |
|
178 |
| "\\<otimes>" => (1.0, "⊗") |
|
179 |
| "\\<bottom>" => (1.0, "⊥") |
|
180 |
| "\\<lceil>" => (1.0, "⌈") |
|
181 |
| "\\<rceil>" => (1.0, "⌉") |
|
182 |
| "\\<lfloor>" => (1.0, "⌊") |
|
183 |
| "\\<rfloor>" => (1.0, "⌋") |
|
184 |
| "\\<langle>" => (1.0, "⟨") |
|
185 |
| "\\<rangle>" => (1.0, "⟩") |
|
186 |
| "\\<lozenge>" => (1.0, "◊") |
|
187 |
| "\\<spadesuit>" => (1.0, "♠") |
|
188 |
| "\\<clubsuit>" => (1.0, "♣") |
|
189 |
| "\\<heartsuit>" => (1.0, "♥") |
|
190 |
| "\\<diamondsuit>" => (1.0, "♦") |
|
191 |
| "\\<lbrakk>" => (2.0, "[|") |
|
192 |
| "\\<rbrakk>" => (2.0, "|]") |
|
193 |
| "\\<Longrightarrow>" => (3.0, "==>") |
|
14571 | 194 |
| "\\<Rightarrow>" => (2.0, "=>") |
14552 | 195 |
| "\\<And>" => (2.0, "!!") |
196 |
| "\\<Colon>" => (2.0, "::") |
|
197 |
| "\\<lparr>" => (2.0, "(|") |
|
198 |
| "\\<rparr>" => (2.0, "|)") |
|
199 |
| "\\<longleftrightarrow>" => (3.0, "<->") |
|
200 |
| "\\<longrightarrow>" => (3.0, "-->") |
|
201 |
| "\\<rightarrow>" => (2.0, "->") |
|
14534 | 202 |
| "\\<^bsub>" => (0.0, "<sub>") |
203 |
| "\\<^esub>" => (0.0, "</sub>") |
|
204 |
| "\\<^bsup>" => (0.0, "<sup>") |
|
205 |
| "\\<^esup>" => (0.0, "</sup>") |
|
14571 | 206 |
| "\\<^sub>" => (0.0, "\\<^sub>") |
14534 | 207 |
| "\\<^sup>" => (0.0, "\\<^sup>") |
14571 | 208 |
| "\\<^isub>" => (0.0, "\\<^isub>") |
14534 | 209 |
| "\\<^isup>" => (0.0, "\\<^isup>") |
14839
c994f1c57fc7
handle raw symbols; Output.add_mode; more robust handling of sub/superscript;
wenzelm
parents:
14775
diff
changeset
|
210 |
| s => |
c994f1c57fc7
handle raw symbols; Output.add_mode; more robust handling of sub/superscript;
wenzelm
parents:
14775
diff
changeset
|
211 |
if Symbol.is_raw s then (1.0, Symbol.decode_raw s) |
c994f1c57fc7
handle raw symbols; Output.add_mode; more robust handling of sub/superscript;
wenzelm
parents:
14775
diff
changeset
|
212 |
else (real (size s), implode (map escape (explode s))); |
6324 | 213 |
|
6338 | 214 |
fun add_sym (width, (w: real, s)) = (width + w, s); |
14534 | 215 |
|
14571 | 216 |
fun script (0, "\\<^sub>") = (1, "<sub>") |
217 |
| script (0, "\\<^isub>") = (1, "<sub>") |
|
218 |
| script (0, "\\<^sup>") = (2, "<sup>") |
|
219 |
| script (0, "\\<^isup>") = (2, "<sup>") |
|
14839
c994f1c57fc7
handle raw symbols; Output.add_mode; more robust handling of sub/superscript;
wenzelm
parents:
14775
diff
changeset
|
220 |
| script (0, x) = (0, x) |
c994f1c57fc7
handle raw symbols; Output.add_mode; more robust handling of sub/superscript;
wenzelm
parents:
14775
diff
changeset
|
221 |
| script (1, x) = (0, x ^ "</sub>") |
c994f1c57fc7
handle raw symbols; Output.add_mode; more robust handling of sub/superscript;
wenzelm
parents:
14775
diff
changeset
|
222 |
| script (2, x) = (0, x ^ "</sup>"); |
14534 | 223 |
|
14839
c994f1c57fc7
handle raw symbols; Output.add_mode; more robust handling of sub/superscript;
wenzelm
parents:
14775
diff
changeset
|
224 |
fun scripts ss = #2 (foldl_map script (0, ss @ [""])); |
6338 | 225 |
in |
6324 | 226 |
|
6338 | 227 |
fun output_width str = |
14992 | 228 |
if not (exists_string (equal "\\" orf equal "<" orf equal ">" orf equal "&") str) |
229 |
then Symbol.default_output str |
|
6338 | 230 |
else |
231 |
let val (width, syms) = foldl_map add_sym (0.0, map output_sym (Symbol.explode str)) |
|
14534 | 232 |
in (implode (scripts syms), width) end; |
6338 | 233 |
|
234 |
val output = #1 o output_width; |
|
14571 | 235 |
val output_symbols = scripts o map (#2 o output_sym); |
6338 | 236 |
|
237 |
end; |
|
238 |
||
6324 | 239 |
|
14973 | 240 |
val _ = Output.add_mode htmlN (output_width, Symbol.default_indent, Symbol.encode_raw); |
6324 | 241 |
|
242 |
||
243 |
(* token translations *) |
|
244 |
||
14541 | 245 |
fun style stl = |
14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
14571
diff
changeset
|
246 |
apfst (enclose ("<span class=" ^ Library.quote stl ^ ">") "</span>") o output_width; |
6324 | 247 |
|
248 |
val html_trans = |
|
14541 | 249 |
[("class", style "tclass"), |
250 |
("tfree", style "tfree"), |
|
251 |
("tvar", style "tvar"), |
|
252 |
("free", style "free"), |
|
253 |
("bound", style "bound"), |
|
254 |
("var", style "var"), |
|
255 |
("xstr", style "xstr")]; |
|
6324 | 256 |
|
257 |
||
258 |
||
259 |
(** HTML markup **) |
|
260 |
||
261 |
type text = string; |
|
262 |
||
263 |
||
264 |
(* atoms *) |
|
265 |
||
266 |
val plain = output; |
|
14541 | 267 |
fun name s = "<span class=\"name\">" ^ output s ^ "</span>"; |
268 |
fun keyword s = "<span class=\"keyword\">" ^ output s ^ "</span>"; |
|
269 |
fun file_name s = "<span class=\"filename\">" ^ output s ^ "</span>"; |
|
6649 | 270 |
val file_path = file_name o Url.pack; |
6324 | 271 |
|
272 |
||
273 |
(* misc *) |
|
274 |
||
14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
14571
diff
changeset
|
275 |
fun href_name s txt = "<a href=" ^ Library.quote s ^ ">" ^ txt ^ "</a>"; |
6649 | 276 |
fun href_path path txt = href_name (Url.pack path) txt; |
6376 | 277 |
|
278 |
fun href_opt_name None txt = txt |
|
279 |
| href_opt_name (Some s) txt = href_name s txt; |
|
280 |
||
281 |
fun href_opt_path None txt = txt |
|
282 |
| href_opt_path (Some p) txt = href_path p txt; |
|
283 |
||
12413 | 284 |
fun para txt = "\n<p>" ^ txt ^ "</p>\n"; |
6324 | 285 |
fun preform txt = "<pre>" ^ txt ^ "</pre>"; |
286 |
val verbatim = preform o output; |
|
287 |
||
288 |
||
289 |
(* document *) |
|
290 |
||
291 |
fun begin_document title = |
|
14083
aed5d25c4a0c
Added DOCTYPE and Content-type to HTML documents.
webertj
parents:
13531
diff
changeset
|
292 |
"<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01 Transitional//EN\" \"http://www.w3.org/TR/html4/loose.dtd\">\n\ |
aed5d25c4a0c
Added DOCTYPE and Content-type to HTML documents.
webertj
parents:
13531
diff
changeset
|
293 |
\\n\ |
aed5d25c4a0c
Added DOCTYPE and Content-type to HTML documents.
webertj
parents:
13531
diff
changeset
|
294 |
\<html>\n\ |
6405 | 295 |
\<head>\n\ |
14083
aed5d25c4a0c
Added DOCTYPE and Content-type to HTML documents.
webertj
parents:
13531
diff
changeset
|
296 |
\<meta http-equiv=\"Content-Type\" content=\"text/html; charset=iso-8859-1\">\n\ |
6405 | 297 |
\<title>" ^ plain (title ^ " (" ^ version ^ ")") ^ "</title>\n\ |
14541 | 298 |
\<link rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\">\n\ |
6405 | 299 |
\</head>\n\ |
300 |
\\n\ |
|
301 |
\<body>\n\ |
|
14541 | 302 |
\<div class=\"head\">\ |
6405 | 303 |
\<h1>" ^ plain title ^ "</h1>\n" |
6324 | 304 |
|
14541 | 305 |
val end_document = "\n</div>\n</body>\n</html>\n"; |
6324 | 306 |
|
6754 | 307 |
fun gen_link how (path, name) = para (href_path path how ^ " to index of " ^ plain name); |
308 |
val up_link = gen_link "Up"; |
|
309 |
val back_link = gen_link "Back"; |
|
6338 | 310 |
|
311 |
||
312 |
(* session index *) |
|
313 |
||
7725 | 314 |
fun begin_index up (index_path, session) opt_readme opt_doc graph = |
6754 | 315 |
begin_document ("Index of " ^ session) ^ up_link up ^ |
316 |
para ("View " ^ href_path graph "theory dependencies" ^ |
|
7725 | 317 |
(case opt_readme of None => "" | Some p => "<br>\nView " ^ href_path p "README") ^ |
318 |
(case opt_doc of None => "" | Some p => "<br>\nView " ^ href_path p "document")) ^ |
|
14541 | 319 |
"\n</div>\n<hr>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n"; |
6338 | 320 |
|
321 |
val end_index = end_document; |
|
322 |
||
6649 | 323 |
fun choice chs s = space_implode " " (map (fn (s', lnk) => |
324 |
enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs); |
|
325 |
||
9415 | 326 |
fun applet_pages session back = |
6649 | 327 |
let |
9415 | 328 |
val sizes = |
329 |
[("small", "small.html", ("500", "400")), |
|
330 |
("medium", "medium.html", ("650", "520")), |
|
331 |
("large", "large.html", ("800", "640"))]; |
|
6649 | 332 |
|
9415 | 333 |
fun applet_page (size, name, (width, height)) = |
6754 | 334 |
let |
335 |
val browser_size = "Set browser size: " ^ |
|
9415 | 336 |
choice (map (fn (y, z, _) => (y, z)) sizes) size; |
6754 | 337 |
in |
338 |
(name, begin_document ("Theory dependencies of " ^ session) ^ |
|
339 |
back_link back ^ |
|
9415 | 340 |
para browser_size ^ |
14541 | 341 |
"\n</div>\n<hr>\n<div class=\"graphbrowser\">\n<applet code=\"GraphBrowser/GraphBrowser.class\" \ |
342 |
\archive=\"GraphBrowser.jar\" \ |
|
9045 | 343 |
\width=" ^ width ^ " height=" ^ height ^ ">\n\ |
9415 | 344 |
\<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\">\n\ |
6754 | 345 |
\</applet>\n<hr>" ^ end_document) |
6649 | 346 |
end; |
9415 | 347 |
in map applet_page sizes end; |
6649 | 348 |
|
349 |
||
6405 | 350 |
fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "\n"; |
351 |
||
6338 | 352 |
val theory_entry = entry; |
353 |
||
6405 | 354 |
fun session_entries [] = "</ul>" |
355 |
| session_entries es = |
|
14541 | 356 |
"</ul>\n</div>\n<hr>\n<div class=\"sessions\">\n<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>"; |
6324 | 357 |
|
358 |
||
359 |
(* theory *) |
|
360 |
||
14571 | 361 |
fun verbatim_source ss = |
362 |
"\n</div>\n<hr>\n<div class=\"source\">\n<pre>" ^ |
|
363 |
implode (output_symbols ss) ^ |
|
364 |
"</pre>\n</div>\n<hr>\n<div class=\"theorems\">\n"; |
|
6324 | 365 |
|
366 |
||
367 |
local |
|
7408 | 368 |
fun encl None = enclose "[" "]" |
369 |
| encl (Some false) = enclose "(" ")" |
|
370 |
| encl (Some true) = I; |
|
6324 | 371 |
|
7408 | 372 |
fun file (opt_ref, path, loadit) = href_opt_path opt_ref (encl loadit (file_path path)); |
7831 | 373 |
val files = space_implode " " o map file; |
6376 | 374 |
val parents = space_implode " + " o map (uncurry href_opt_path o apsnd name); |
6361 | 375 |
|
6376 | 376 |
fun theory up A = |
377 |
begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^ |
|
6324 | 378 |
keyword "theory" ^ " " ^ name A ^ " = "; |
379 |
in |
|
380 |
||
6376 | 381 |
fun begin_theory up A Bs [] body = theory up A ^ parents Bs ^ ":\n" ^ body |
12413 | 382 |
| begin_theory up A Bs Ps body = theory up A ^ parents Bs ^ "<br>\n" ^ keyword "files" ^ |
6376 | 383 |
" " ^ files Ps ^ ":" ^ "\n" ^ body; |
6324 | 384 |
end; |
385 |
||
6338 | 386 |
val end_theory = end_document; |
6324 | 387 |
|
388 |
||
389 |
(* ML file *) |
|
390 |
||
391 |
fun ml_file path str = |
|
6649 | 392 |
begin_document ("File " ^ Url.pack path) ^ |
14571 | 393 |
"\n</div>\n<hr><div class=\"mlsource\">\n" ^ |
394 |
verbatim str ^ |
|
395 |
"\n</div>\n<hr>\n<div class=\"mlfooter\">\n" ^ |
|
14541 | 396 |
end_document; |
6324 | 397 |
|
398 |
||
7408 | 399 |
(* theorems *) |
6324 | 400 |
|
7572 | 401 |
local |
402 |
||
7408 | 403 |
val string_of_thm = |
14839
c994f1c57fc7
handle raw symbols; Output.add_mode; more robust handling of sub/superscript;
wenzelm
parents:
14775
diff
changeset
|
404 |
Output.output o Pretty.setmp_margin 80 Pretty.string_of o |
6324 | 405 |
Display.pretty_thm_no_quote o #1 o Drule.freeze_thaw; |
406 |
||
407 |
fun thm th = preform (prefix_lines " " (html_mode string_of_thm th)); |
|
7408 | 408 |
|
7572 | 409 |
fun thm_name "" = "" |
410 |
| thm_name a = " " ^ name (a ^ ":"); |
|
411 |
||
412 |
in |
|
413 |
||
13531 | 414 |
fun result k (a, ths) = para (cat_lines ((keyword k ^ thm_name a) :: map thm ths)); |
7572 | 415 |
|
13531 | 416 |
fun results _ [] = "" |
417 |
| results k (res :: ress) = cat_lines (result k res :: map (result "and") ress); |
|
7572 | 418 |
|
419 |
end; |
|
6324 | 420 |
|
421 |
||
7634 | 422 |
(* sections *) |
6324 | 423 |
|
8088 | 424 |
fun chapter heading = "\n\n<h1>" ^ plain heading ^ "</h1>\n"; |
6324 | 425 |
fun section heading = "\n\n<h2>" ^ plain heading ^ "</h2>\n"; |
7634 | 426 |
fun subsection heading = "\n\n<h3>" ^ plain heading ^ "</h3>\n"; |
427 |
fun subsubsection heading = "\n\n<h4>" ^ plain heading ^ "</h4>\n"; |
|
6324 | 428 |
|
429 |
||
430 |
(** theory setup **) |
|
431 |
||
432 |
val setup = |
|
433 |
[Theory.add_mode_tokentrfuns htmlN html_trans]; |
|
434 |
||
435 |
||
436 |
end; |