equal
deleted
inserted
replaced
199 close_in instream |
199 close_in instream |
200 end; |
200 end; |
201 |
201 |
202 fun file_exists file = (file_info file <> ""); |
202 fun file_exists file = (file_info file <> ""); |
203 |
203 |
|
204 (*Get last directory in path (e.g. /usr/proj/isabelle -> isabelle) *) |
|
205 fun last_path s = case space_explode "/" s of |
|
206 [] => "" |
|
207 | ds => last_elem ds; |
|
208 |
204 (*Get thy_info for a loaded theory *) |
209 (*Get thy_info for a loaded theory *) |
205 fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname); |
210 fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname); |
206 |
211 |
207 (*Check if a theory was completly loaded *) |
212 (*Check if a theory was completly loaded *) |
208 fun already_loaded thy = |
213 fun already_loaded thy = |
400 if (!index_path) = "" then |
405 if (!index_path) = "" then |
401 error "index_path is empty. Please use 'init_html()' instead of \ |
406 error "index_path is empty. Please use 'init_html()' instead of \ |
402 \'make_html := true'" |
407 \'make_html := true'" |
403 else if (!index_path) subdir_of (!base_path) then |
408 else if (!index_path) subdir_of (!base_path) then |
404 relative_path (!base_path) (!index_path) |
409 relative_path (!base_path) (!index_path) |
405 else |
410 else last_path (!index_path); |
406 last_elem (space_explode "/" (!index_path)); |
|
407 val rel_index_path = relative_path tpath (!index_path); |
411 val rel_index_path = relative_path tpath (!index_path); |
408 |
412 |
409 (*Make list of all theories and all theories that own a .thy file*) |
413 (*Make list of all theories and all theories that own a .thy file*) |
410 fun list_theories [] theories thy_files = (theories, thy_files) |
414 fun list_theories [] theories thy_files = (theories, thy_files) |
411 | list_theories ((tname, ThyInfo {thy_time, ...}) :: ts) |
415 | list_theories ((tname, ThyInfo {thy_time, ...}) :: ts) |
682 tack_on gif_path "blue_arrow.gif\" ALT = /\\></A>\n"); |
686 tack_on gif_path "blue_arrow.gif\" ALT = /\\></A>\n"); |
683 close_out out |
687 close_out out |
684 end; |
688 end; |
685 |
689 |
686 val theory_list = |
690 val theory_list = |
687 open_append (tack_on (!index_path) ".theory_list.txt"); |
691 open_append (tack_on (!index_path) ".theory_list.txt") |
|
692 handle _ => (make_html := false; |
|
693 writeln ("Warning: Cannot write to " ^ |
|
694 (!index_path) ^ " while making HTML files.\n\ |
|
695 \HTML generation has been switched off.\n\ |
|
696 \Call init_html() from within a \ |
|
697 \writeable directory to reactivate it."); |
|
698 raise MK_HTML) |
688 in output (theory_list, tname ^ " " ^ abs_path ^ "\n"); |
699 in output (theory_list, tname ^ " " ^ abs_path ^ "\n"); |
689 close_out theory_list; |
700 close_out theory_list; |
690 |
701 |
691 robust_seq add_to_parents new_parents |
702 robust_seq add_to_parents new_parents |
692 end |
703 end |
749 |
760 |
750 (*Add theory to list of all loaded theories (for index.html) |
761 (*Add theory to list of all loaded theories (for index.html) |
751 and add it to its parents' sub-charts*) |
762 and add it to its parents' sub-charts*) |
752 if !make_html then |
763 if !make_html then |
753 let val path = path_of tname; |
764 let val path = path_of tname; |
754 in if path = "" then mk_html () (*first time theory has been read*) |
765 in if path = "" then (*first time theory has been read*) |
|
766 (mk_html() handle MK_HTML => ()) |
755 else () |
767 else () |
756 end |
768 end |
757 else (); |
769 else (); |
758 |
770 |
759 (*Now set the correct info*) |
771 (*Now set the correct info*) |
1142 let val pure_out = open_out ".Pure_sub.html"; |
1154 let val pure_out = open_out ".Pure_sub.html"; |
1143 val cpure_out = open_out ".CPure_sub.html"; |
1155 val cpure_out = open_out ".CPure_sub.html"; |
1144 val package = |
1156 val package = |
1145 if cwd subdir_of (!base_path) then |
1157 if cwd subdir_of (!base_path) then |
1146 relative_path (!base_path) cwd |
1158 relative_path (!base_path) cwd |
1147 else |
1159 else last_path cwd; |
1148 last_elem (space_explode "/" cwd); |
|
1149 in mk_charthead pure_out "Pure" "Children" false rel_gif_path "" |
1160 in mk_charthead pure_out "Pure" "Children" false rel_gif_path "" |
1150 package; |
1161 package; |
1151 mk_charthead cpure_out "CPure" "Children" false rel_gif_path "" |
1162 mk_charthead cpure_out "CPure" "Children" false rel_gif_path "" |
1152 package; |
1163 package; |
1153 output (pure_out, "Pure\n"); |
1164 output (pure_out, "Pure\n"); |
1208 index.html is placed; if index_path is no subdirectory of base_path |
1219 index.html is placed; if index_path is no subdirectory of base_path |
1209 then take the last directory of index_path*) |
1220 then take the last directory of index_path*) |
1210 val inside_isabelle = (!index_path) subdir_of (!base_path); |
1221 val inside_isabelle = (!index_path) subdir_of (!base_path); |
1211 val subdir = |
1222 val subdir = |
1212 if inside_isabelle then relative_path (!base_path) (!index_path) |
1223 if inside_isabelle then relative_path (!base_path) (!index_path) |
1213 else last_elem (space_explode "/" (!index_path)); |
1224 else last_path (!index_path); |
1214 val subdirs = space_explode "/" subdir; |
1225 val subdirs = space_explode "/" subdir; |
1215 |
1226 |
1216 (*Look for index.html in superdirectories; stop when Isabelle's |
1227 (*Look for index.html in superdirectories; stop when Isabelle's |
1217 main directory is reached*) |
1228 main directory is reached*) |
1218 fun find_super_index [] n = ("", n) |
1229 fun find_super_index [] n = ("", n) |