\nBack to the index of " ^ package ^ "\n
\n
");
(*Convert .thy file to HTML and make chart of its super-theories*)
fun thyfile2html tpath tname =
let
val gif_path = relative_path tpath (!gif_path);
val package =
- case rev (space_explode "/" (!index_path)) of
- x::xs => x
- | _ => error "index_path is empty. \
- \Please use 'init_html()' instead of \
- \'make_html := true'";
- val index_path = relative_path tpath (!index_path);
+ if (!index_path) = "" then
+ error "index_path is empty. Please use 'init_html()' instead of \
+ \'make_html := true'"
+ else relative_path (!base_path) (!index_path);
+ val rel_index_path = relative_path tpath (!index_path);
(*Make list of all theories and all theories that own a .thy file*)
fun list_theories [] theories thy_files = (theories, thy_files)
@@ -408,11 +437,10 @@
in (implode pre ^ ancestors, body) end;
in "" ^ tname ^ ".thy \n\n\n" ^
"" ^ tname ^ ".thy
\nBack to the main theory chart of " ^ package ^
- ".\n
\n\n\n" ^ comment ^ ancestors ^ body ^
- "
\n
Theorems proved in " ^ tname ^ ".ML:
\n"
+ tack_on rel_index_path "index.html\
+ \\">Back to the index of " ^ package ^
+ "\n
\n\n\n" ^ comment ^ ancestors ^ body ^
+ "
\n"
end;
(** Make chart of super-theories **)
@@ -427,16 +455,16 @@
filter (fn s => s mem thy_files orelse s = "Pure" orelse s = "CPure")
theories;
- (*Make nested list of theories*)
+ (*Make tree of theory dependencies*)
fun list_ancestors tname level continued =
let
fun mk_entry [] = ()
| mk_entry (t::ts) =
let
val is_pure = t = "Pure" orelse t = "CPure";
- val path = path_of t;
- val rel_path = if is_pure then index_path
- else relative_path tpath path;
+ val path = if is_pure then (the (!pure_subchart))
+ else path_of t;
+ val rel_path = relative_path tpath path;
val repeated = t mem (!listed) andalso not (null (parents_of t));
fun mk_offset [] cur =
@@ -474,9 +502,12 @@
error "thyfile2html: Last theory's HTML file has not been closed."
else ();
cur_htmlfile := Some (open_out (tack_on tpath ("." ^ tname ^ ".html")));
+ cur_has_title := false;
+ cur_name := tname;
output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy"));
- mk_charthead sup_out tname "Ancestors" true gif_path index_path package;
+ mk_charthead sup_out tname "Ancestors" true gif_path rel_index_path
+ package;
output(sup_out,
"" ^ tname ^ " \
\
");
close_out sup_out;
- mk_charthead sub_out tname "Children" false gif_path index_path package;
+ mk_charthead sub_out tname "Children" false gif_path rel_index_path
+ package;
output(sub_out,
"" ^ tname ^ " \
\![](\"")
- output (out, "" ^ name ^ "\n" ^
- escape (explode (string_of_thm (freeze thm))) ^
- "
\n")
+ (if not (!cur_has_title) then
+ (cur_has_title := true;
+ output (out, "
Theorems proved in " ^ (!cur_name) ^
+ ".ML:
\n"))
+ else ();
+ output (out, "" ^ name ^ "\n" ^
+ escape (explode (string_of_thm (freeze thm))) ^
+ "
\n")
+ )
| None => ()
end;
in
@@ -1000,71 +1040,94 @@
(*Init HTML generator by setting paths and creating new files*)
fun init_html () =
- let val pure_out = open_out ".Pure_sub.html";
- val cpure_out = open_out ".CPure_sub.html";
+ let val cwd = pwd();
+
val theory_list = close_out (open_out ".theory_list.txt");
- val rel_gif_path = relative_path (pwd ()) (!gif_path);
- val package = hd (rev (space_explode "/" (pwd ())));
+ val rel_gif_path = relative_path cwd (!gif_path);
+ val package = relative_path (!base_path) cwd;
+
+ (*Make new HTML files for Pure and CPure*)
+ fun init_pure_html () =
+ let val pure_out = open_out ".Pure_sub.html";
+ val cpure_out = open_out ".CPure_sub.html";
+ in mk_charthead pure_out "Pure" "Children" false rel_gif_path ""
+ package;
+ mk_charthead cpure_out "CPure" "Children" false rel_gif_path ""
+ package;
+ output (pure_out, "Pure\n");
+ output (cpure_out, "CPure\n");
+ close_out pure_out;
+ close_out cpure_out;
+ pure_subchart := Some cwd
+ end;
in make_html := true;
- index_path := pwd();
- writeln ("Setting path for index.html to " ^ quote (!index_path) ^
+ index_path := cwd;
+
+ writeln ("Setting path for index.html to " ^ quote cwd ^
"\nGIF path has been set to " ^ quote (!gif_path));
- mk_charthead pure_out "Pure" "Children" false rel_gif_path "" package;
- mk_charthead cpure_out "CPure" "Children" false rel_gif_path "" package;
- output (pure_out, "Pure\n");
- output (cpure_out, "CPure\n");
- close_out pure_out;
- close_out cpure_out
+ if is_none (!pure_subchart) then init_pure_html()
+ else ()
end;
(*Generate index.html*)
fun make_chart () = if not (!make_html) then () else
- let val theory_list = open_in (tack_on (!index_path) ".theory_list.txt");
+ let val tlist_path = tack_on (!index_path) ".theory_list.txt";
+ val theory_list = open_in tlist_path;
val theories = space_explode "\n" (input (theory_list, 999999));
- val dummy = close_in theory_list;
-
- (*Path to Isabelle's main directory = $gif_path/.. *)
- val base_path = "/" ^
- space_implode "/" (rev (tl (rev (space_explode "/" (!gif_path)))));
+ val dummy = (close_in theory_list; delete_file tlist_path);
val gif_path = relative_path (!index_path) (!gif_path);
(*Make entry for main chart of all theories.*)
- fun main_entries [] curdir =
- implode (replicate (length curdir -1) "\n")
- | main_entries (t::ts) curdir =
- let
- val (name, path) = take_prefix (not_equal " ") (explode t);
+ fun main_entry t =
+ let
+ val (name, path) = take_prefix (not_equal " ") (explode t);
- val tname = implode name
- val tpath =
- tack_on (relative_path (!index_path) (implode (tl path)))
- ("." ^ tname);
- val subdir = space_explode "/"
- (relative_path base_path (implode (tl path)));
- val level_diff = length subdir - length curdir;
- in "\n" ^
- (if subdir <> curdir then
- (implode (if level_diff > 0 then
- replicate level_diff "
\n"
- else if level_diff < 0 then
- replicate (~level_diff) "
\n"
- else []) ^
- "" ^ space_implode "/" subdir ^ "
\n")
- else "") ^
- "" ^
- " " ^ tname ^ "
\n" ^
- main_entries ts subdir
- end;
+ val tname = implode name
+ val tpath = tack_on (relative_path (!index_path) (implode (tl path)))
+ ("." ^ tname);
+ in "" ^
+ " " ^ tname ^ "
\n"
+ end;
val out = open_out (tack_on (!index_path) "index.html");
- val subdir = relative_path base_path (!index_path);
+ val subdir = relative_path (!base_path) (!index_path);
+ val subdirs = space_explode "/" subdir;
+
+ (*Look for index.html in superdirectories*)
+ fun find_super_index [] _ =
+ error "make_chart: Unable to find super index file."
+ | find_super_index (p::ps) n =
+ let val index_path = "/" ^ space_implode "/" (rev ps);
+ in if file_exists (index_path ^ "/index.html") then (index_path, n)
+ else find_super_index ps (n+1)
+ end;
+ val (super_index, level_diff) =
+ find_super_index (rev (space_explode "/" (!index_path))) 1;
+ val level = length subdirs - level_diff;
+
+ (*Add link to current directory to 'super' index.html*)
+ fun link_directory () =
+ let val old_index = open_in (super_index ^ "/index.html");
+ val content = rev (explode (input (old_index, 999999)));
+ val dummy = close_in old_index;
+
+ val out = open_append (super_index ^ "/index.html");
+ val rel_path = space_implode "/" (drop (level, subdirs));
+ in
+ output (out,
+ (if nth_elem (3, content) <> "!" then ""
+ else "\n
Subdirectories:
\n") ^
+ "" ^ rel_path ^
+ "
\n");
+ close_out out
+ end;
in output (out,
"Isabelle/" ^ subdir ^ " \n\
\Isabelle/" ^ subdir ^ "
\n\
@@ -1072,17 +1135,33 @@
\ stands for subtheories (child theories)
\n\
\ stands for supertheories (parent theories)\n\
- \\
- \Back to the index of Isabelle logics.\n" ^
- (if file_exists "README.html" then
+ \\" ALT = /\\> stands for supertheories (parent theories)\
+ \
\nBack to the index of " ^
+ (if level = 0 then "Isabelle logics"
+ else space_implode "/" (take (level, subdirs))) ^
+ "\n" ^
+ (if file_exists (tack_on (!index_path) "README.html") then
"
View the ReadMe file.\n"
- else if file_exists "README" then
+ else if file_exists (tack_on (!index_path) "README") then
"
View the ReadMe file.\n"
else "") ^
- "
" ^ main_entries theories (space_explode "/" base_path) ^
- "\n");
- close_out out
+ "
" ^ implode (map main_entry theories) ^ "");
+ close_out out;
+ if level = 0 then () else link_directory ()
end;
+
+(*CD to a directory and load its ROOT.ML file*)
+fun use_dir dirname =
+ (cd dirname;
+ if !make_html then init_html() else ();
+ use "ROOT.ML";
+ make_chart());
+
+fun exit_use_dir dirname =
+ (cd dirname;
+ if !make_html then init_html() else ();
+ exit_use "ROOT.ML";
+ make_chart());
+
end;