268 |
267 |
269 fun href_opt_path NONE txt = txt |
268 fun href_opt_path NONE txt = txt |
270 | href_opt_path (SOME p) txt = href_path p txt; |
269 | href_opt_path (SOME p) txt = href_path p txt; |
271 |
270 |
272 fun para txt = "\n<p>" ^ txt ^ "</p>\n"; |
271 fun para txt = "\n<p>" ^ txt ^ "</p>\n"; |
273 fun preform txt = "<pre>" ^ txt ^ "</pre>"; |
272 fun preform txt = "<pre xml:space=\"preserve\">" ^ txt ^ "</pre>"; |
274 val verbatim = preform o output; |
273 val verbatim = preform o output; |
275 |
274 |
276 |
275 |
277 (* document *) |
276 (* document *) |
278 |
277 |
279 val charset = ref "iso-8859-1"; |
278 val charset = ref "ISO-8859-1"; |
280 fun with_charset s = setmp_noncritical charset s; |
279 fun with_charset s = setmp_noncritical charset s; |
281 |
280 |
282 fun begin_document title = |
281 fun begin_document title = |
283 "<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01 Transitional//EN\" \ |
282 let val cs = ! charset in |
284 \\"http://www.w3.org/TR/html4/loose.dtd\">\n\ |
283 "<?xml version=\"1.0\" encoding=\"" ^ cs ^ "\" ?>\n\ |
285 \\n\ |
284 \<!DOCTYPE HTML PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \ |
286 \<html>\n\ |
285 \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\ |
287 \<head>\n\ |
286 \<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\ |
288 \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=" ^ ! charset ^ "\">\n\ |
287 \<head>\n\ |
289 \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\ |
288 \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=" ^ cs ^ "\"/>\n\ |
290 \<link rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\">\n\ |
289 \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\ |
291 \</head>\n\ |
290 \<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\ |
292 \\n\ |
291 \</head>\n\ |
293 \<body>\n\ |
292 \\n\ |
294 \<div class=\"head\">\ |
293 \<body>\n\ |
295 \<h1>" ^ plain title ^ "</h1>\n" |
294 \<div class=\"head\">\ |
|
295 \<h1>" ^ plain title ^ "</h1>\n" |
|
296 end; |
296 |
297 |
297 val end_document = "\n</div>\n</body>\n</html>\n"; |
298 val end_document = "\n</div>\n</body>\n</html>\n"; |
298 |
299 |
299 fun gen_link how (path, name) = para (href_path path how ^ " to index of " ^ plain name); |
300 fun gen_link how (path, name) = para (href_path path how ^ " to index of " ^ plain name); |
300 val up_link = gen_link "Up"; |
301 val up_link = gen_link "Up"; |
304 (* session index *) |
305 (* session index *) |
305 |
306 |
306 fun begin_index up (index_path, session) docs graph = |
307 fun begin_index up (index_path, session) docs graph = |
307 begin_document ("Index of " ^ session) ^ up_link up ^ |
308 begin_document ("Index of " ^ session) ^ up_link up ^ |
308 para ("View " ^ href_path graph "theory dependencies" ^ |
309 para ("View " ^ href_path graph "theory dependencies" ^ |
309 implode (map (fn (p, name) => "<br>\nView " ^ href_path p name) docs)) ^ |
310 implode (map (fn (p, name) => "<br/>\nView " ^ href_path p name) docs)) ^ |
310 "\n</div>\n<hr>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n"; |
311 "\n</div>\n<hr/>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n"; |
311 |
312 |
312 val end_index = end_document; |
313 val end_index = end_document; |
313 |
314 |
314 fun choice chs s = space_implode " " (map (fn (s', lnk) => |
315 fun choice chs s = space_implode " " (map (fn (s', lnk) => |
315 enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs); |
316 enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs); |
327 choice (map (fn (y, z, _) => (y, z)) sizes) size; |
328 choice (map (fn (y, z, _) => (y, z)) sizes) size; |
328 in |
329 in |
329 (name, begin_document ("Theory dependencies of " ^ session) ^ |
330 (name, begin_document ("Theory dependencies of " ^ session) ^ |
330 back_link back ^ |
331 back_link back ^ |
331 para browser_size ^ |
332 para browser_size ^ |
332 "\n</div>\n<hr>\n<div class=\"graphbrowser\">\n\ |
333 "\n</div>\n<hr/>\n<div class=\"graphbrowser\">\n\ |
333 \<applet code=\"GraphBrowser/GraphBrowser.class\" \ |
334 \<applet code=\"GraphBrowser/GraphBrowser.class\" \ |
334 \archive=\"GraphBrowser.jar\" \ |
335 \archive=\"GraphBrowser.jar\" \ |
335 \width=" ^ width ^ " height=" ^ height ^ ">\n\ |
336 \width=" ^ width ^ " height=" ^ height ^ ">\n\ |
336 \<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\">\n\ |
337 \<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\">\n\ |
337 \</applet>\n<hr>" ^ end_document) |
338 \</applet>\n<hr/>" ^ end_document) |
338 end; |
339 end; |
339 in map applet_page sizes end; |
340 in map applet_page sizes end; |
340 |
341 |
341 |
342 |
342 fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "\n"; |
343 fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\n"; |
343 |
344 |
344 val theory_entry = entry; |
345 val theory_entry = entry; |
345 |
346 |
346 fun session_entries [] = "</ul>" |
347 fun session_entries [] = "</ul>" |
347 | session_entries es = |
348 | session_entries es = |
348 "</ul>\n</div>\n<hr>\n<div class=\"sessions\">\n\ |
349 "</ul>\n</div>\n<hr/>\n<div class=\"sessions\">\n\ |
349 \<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>"; |
350 \<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>"; |
350 |
351 |
351 |
352 |
352 (* theory *) |
353 (* theory *) |
353 |
354 |
354 fun verbatim_source ss = |
355 fun verbatim_source ss = |
355 "\n</div>\n<hr>\n<div class=\"source\">\n<pre>" ^ |
356 "\n</div>\n<hr/>\n<div class=\"source\">\n<pre xml:space=\"preserve\">" ^ |
356 implode (output_symbols ss) ^ |
357 implode (output_symbols ss) ^ |
357 "</pre>\n</div>\n<hr>\n<div class=\"theorems\">\n"; |
358 "</pre>\n</div>\n<hr/>\n<div class=\"theorems\">\n"; |
358 |
359 |
359 |
360 |
360 local |
361 local |
361 fun file (href, path, loadit) = |
362 fun file (href, path, loadit) = |
362 href_path href (if loadit then file_path path else enclose "(" ")" (file_path path)); |
363 href_path href (if loadit then file_path path else enclose "(" ")" (file_path path)); |
366 command "theory" ^ " " ^ name A; |
367 command "theory" ^ " " ^ name A; |
367 |
368 |
368 fun imports Bs = |
369 fun imports Bs = |
369 keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs); |
370 keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs); |
370 |
371 |
371 fun uses Ps = keyword "uses" ^ " " ^ space_implode " " (map file Ps) ^ "<br>\n"; |
372 fun uses Ps = keyword "uses" ^ " " ^ space_implode " " (map file Ps) ^ "<br/>\n"; |
372 in |
373 in |
373 |
374 |
374 fun begin_theory up A Bs Ps body = |
375 fun begin_theory up A Bs Ps body = |
375 theory up A ^ "<br>\n" ^ |
376 theory up A ^ "<br/>\n" ^ |
376 imports Bs ^ "<br>\n" ^ |
377 imports Bs ^ "<br/>\n" ^ |
377 (if null Ps then "" else uses Ps) ^ |
378 (if null Ps then "" else uses Ps) ^ |
378 keyword "begin" ^ "<br>\n" ^ |
379 keyword "begin" ^ "<br/>\n" ^ |
379 body; |
380 body; |
380 |
381 |
381 end; |
382 end; |
382 |
383 |
383 val end_theory = end_document; |
384 val end_theory = end_document; |