307 (sup if this head is for a sub-chart, sub if it is for a sup-chart; |
307 (sup if this head is for a sub-chart, sub if it is for a sup-chart; |
308 empty for Pure and CPure sub-charts) |
308 empty for Pure and CPure sub-charts) |
309 gif_path: relative path to directory containing GIFs |
309 gif_path: relative path to directory containing GIFs |
310 index_path: relative path to directory containing main theory chart |
310 index_path: relative path to directory containing main theory chart |
311 *) |
311 *) |
312 fun mk_charthead file tname title green_arrow gif_path index_path package = |
312 fun mk_charthead file tname title repeats gif_path index_path package = |
313 output (file, |
313 output (file, |
314 "<HTML><HEAD><TITLE>" ^ title ^ " of " ^ tname ^ |
314 "<HTML><HEAD><TITLE>" ^ title ^ " of " ^ tname ^ |
315 "</TITLE></HEAD>\n<H2>" ^ title ^ " of theory " ^ tname ^ |
315 "</TITLE></HEAD>\n<H2>" ^ title ^ " of theory " ^ tname ^ |
316 "</H2>\nThe name of every theory is linked to its theory file<BR>\n" ^ |
316 "</H2>\nThe name of every theory is linked to its theory file<BR>\n" ^ |
317 "<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\ |
317 "<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\ |
318 \\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\ |
318 \\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\ |
319 \<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\ |
319 \<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\ |
320 \\" ALT = /\\></A> stands for supertheories (parent theories)\n" ^ |
320 \\" ALT = /\\></A> stands for supertheories (parent theories)\n" ^ |
321 (if not green_arrow then "" else |
321 (if not repeats then "" else |
322 "<BR><IMG SRC = \"" ^ tack_on gif_path "green_arrow.gif\ |
322 "<BR><TT>...</TT> stands for repeated subtrees") ^ |
323 \\" ALT = >></A> stands for repeated subtrees") ^ |
|
324 "<P><A HREF = \"" ^ tack_on index_path "index.html\ |
323 "<P><A HREF = \"" ^ tack_on index_path "index.html\ |
325 \\">Back</A> to the main theory chart of " ^ package ^ ".\n<HR>\n<PRE>"); |
324 \\">Back</A> to the main theory chart of " ^ package ^ ".\n<HR>\n<PRE>"); |
326 |
325 |
327 (*Convert .thy file to HTML and make chart of its super-theories*) |
326 (*Convert .thy file to HTML and make chart of its super-theories*) |
328 fun thyfile2html tpath tname = |
327 fun thyfile2html tpath tname = |
329 let |
328 let |
330 val gif_path = relative_path tpath (!gif_path); |
329 val gif_path = relative_path tpath (!gif_path); |
331 val package = hd (rev (space_explode "/" (!index_path))); |
330 val package = |
|
331 case rev (space_explode "/" (!index_path)) of |
|
332 x::xs => x |
|
333 | _ => error "index_path is empty. \ |
|
334 \Please use 'init_html()' instead of \ |
|
335 \'make_html := true'"; |
332 val index_path = relative_path tpath (!index_path); |
336 val index_path = relative_path tpath (!index_path); |
333 |
337 |
334 (*Make list of all theories and all theories that own a .thy file*) |
338 (*Make list of all theories and all theories that own a .thy file*) |
335 fun list_theories [] theories thy_files = (theories, thy_files) |
339 fun list_theories [] theories thy_files = (theories, thy_files) |
336 | list_theories ((tname, ThyInfo {thy_time, ...}) :: ts) |
340 | list_theories ((tname, ThyInfo {thy_time, ...}) :: ts) |
431 let |
435 let |
432 val is_pure = t = "Pure" orelse t = "CPure"; |
436 val is_pure = t = "Pure" orelse t = "CPure"; |
433 val path = path_of t; |
437 val path = path_of t; |
434 val rel_path = if is_pure then index_path |
438 val rel_path = if is_pure then index_path |
435 else relative_path tpath path; |
439 else relative_path tpath path; |
|
440 val repeated = t mem (!listed) andalso not (null (parents_of t)); |
436 |
441 |
437 fun mk_offset [] cur = |
442 fun mk_offset [] cur = |
438 if level < cur then error "Error in mk_offset" |
443 if level < cur then error "Error in mk_offset" |
439 else implode (replicate (level - cur) " ") |
444 else implode (replicate (level - cur) " ") |
440 | mk_offset (l::ls) cur = |
445 | mk_offset (l::ls) cur = |
442 mk_offset ls (l+1); |
447 mk_offset ls (l+1); |
443 in output (sup_out, |
448 in output (sup_out, |
444 " " ^ mk_offset continued 0 ^ |
449 " " ^ mk_offset continued 0 ^ |
445 "\\__" ^ (if is_pure then t else "<A HREF=\"" ^ |
450 "\\__" ^ (if is_pure then t else "<A HREF=\"" ^ |
446 tack_on rel_path t ^ ".html\">" ^ t ^ "</A>") ^ |
451 tack_on rel_path t ^ ".html\">" ^ t ^ "</A>") ^ |
447 " <A HREF = \"" ^ tack_on rel_path t ^ |
452 (if repeated then "..." else " ") ^ |
448 "_sub.html\"><IMG ALIGN=TOP SRC = \"" ^ |
453 "<A HREF = \"" ^ tack_on rel_path t ^ |
|
454 "_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
449 tack_on gif_path "red_arrow.gif\" ALT = \\/></A>" ^ |
455 tack_on gif_path "red_arrow.gif\" ALT = \\/></A>" ^ |
450 (if is_pure then "" |
456 (if is_pure then "" |
451 else "<A HREF = \"" ^ tack_on rel_path t ^ |
457 else "<A HREF = \"" ^ tack_on rel_path t ^ |
452 "_sup.html\"><IMG ALIGN=TOP SRC = \"" ^ |
458 "_sup.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
453 tack_on gif_path "blue_arrow.gif\ |
459 tack_on gif_path "blue_arrow.gif\ |
454 \\" ALT = /\\></A>")); |
460 \\" ALT = /\\></A>") ^ |
455 if t mem (!listed) andalso not (null (parents_of t)) then |
461 "\n"); |
456 output (sup_out, |
462 if repeated then () |
457 "<A HREF = \"" ^ tack_on rel_path t ^ "_sup.html\">\ |
463 else (listed := t :: (!listed); |
458 \<IMG ALIGN=TOP SRC = \"" ^ |
|
459 tack_on gif_path "green_arrow.gif\" ALT = >></A>\n") |
|
460 else (output (sup_out, "\n"); |
|
461 listed := t :: (!listed); |
|
462 list_ancestors t (level+1) (if null ts then continued |
464 list_ancestors t (level+1) (if null ts then continued |
463 else continued @ [level]); |
465 else continued @ [level]); |
464 mk_entry ts) |
466 mk_entry ts) |
465 end; |
467 end; |
466 |
468 |
474 output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy")); |
476 output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy")); |
475 |
477 |
476 mk_charthead sup_out tname "Ancestors" true gif_path index_path package; |
478 mk_charthead sup_out tname "Ancestors" true gif_path index_path package; |
477 output(sup_out, |
479 output(sup_out, |
478 "<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \ |
480 "<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \ |
479 \<A HREF = \"" ^ tname ^ "_sub.html\"><IMG ALIGN=TOP SRC = \"" ^ |
481 \<A HREF = \"" ^ tname ^ |
|
482 "_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
480 tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\n"); |
483 tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\n"); |
481 list_ancestors tname 0 []; |
484 list_ancestors tname 0 []; |
482 output (sup_out, "</PRE><HR></BODY></HTML>"); |
485 output (sup_out, "</PRE><HR></BODY></HTML>"); |
483 close_out sup_out; |
486 close_out sup_out; |
484 |
487 |
485 mk_charthead sub_out tname "Children" false gif_path index_path package; |
488 mk_charthead sub_out tname "Children" false gif_path index_path package; |
486 output(sub_out, |
489 output(sub_out, |
487 "<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \ |
490 "<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \ |
488 \<A HREF = \"" ^ tname ^ "_sup.html\"><IMG SRC = \"" ^ |
491 \<A HREF = \"" ^ tname ^ "_sup.html\"><IMG SRC = \"" ^ |
489 tack_on gif_path "blue_arrow.gif\" ALT = \\/></A>\n"); |
492 tack_on gif_path "blue_arrow.gif\" BORDER=0 ALT = \\/></A>\n"); |
490 close_out sub_out |
493 close_out sub_out |
491 end; |
494 end; |
492 |
495 |
493 |
496 |
494 (*Read .thy and .ML files that haven't been read yet or have changed since |
497 (*Read .thy and .ML files that haven't been read yet or have changed since |
596 val out = open_append (tack_on path t ^ "_sub.html"); |
599 val out = open_append (tack_on path t ^ "_sub.html"); |
597 in output (out, |
600 in output (out, |
598 " |\n \\__<A HREF=\"" ^ tack_on rel_path tname ^ ".html\">" ^ |
601 " |\n \\__<A HREF=\"" ^ tack_on rel_path tname ^ ".html\">" ^ |
599 tname ^ "</A> <A HREF = \"" ^ |
602 tname ^ "</A> <A HREF = \"" ^ |
600 tack_on rel_path tname ^ |
603 tack_on rel_path tname ^ |
601 "_sub.html\"><IMG ALIGN=TOP SRC = \"" ^ |
604 "_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
602 tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\ |
605 tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\ |
603 \<A HREF = \"" ^ tack_on rel_path tname ^ "_sup.html\">\ |
606 \<A HREF = \"" ^ tack_on rel_path tname ^ "_sup.html\">\ |
604 \<IMG ALIGN=TOP SRC = \"" ^ tack_on gif_path "blue_arrow.gif\ |
607 \<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
605 \\" ALT = /\\></A>\n"); |
608 tack_on gif_path "blue_arrow.gif\" ALT = /\\></A>\n"); |
606 close_out out |
609 close_out out |
607 end; |
610 end; |
608 |
611 |
609 val theory_list = |
612 val theory_list = |
610 open_append (tack_on (!index_path) "theory_list.txt"); |
613 open_append (tack_on (!index_path) "theory_list.txt"); |