"^name^"\n"^
- " \n![(sub)](\""^srcpath^)
\n"^
- "\n\n"^
- "\n"^
- join(dependencies(name,mat),"")^
- "
\n"
- in
- map maketableentry stringlist
- end;
-
-
-
-(* --------------------
- Create individual super- and sub-theory charts for
- each theory. Store them in separate files.
- It contains the subfunction:
- - page
- -------------------- *)
-
-fun pages ([],_,_,_) = 0
- | pages (th::theories,theorymatrix,suffix,headline) =
- let
- fun page th =
- let
-
- (* Open files for output of individual charts. *)
-
- val outf_each = open_out (htmlpath^th^"_"^suffix^".html")
- in
-
- (* Recursively write to the output files the *)
- (* dependent theories with appropriate links *)
- (* depending upon the suffix. *)
-
- output(outf_each,
-
- (* Heading of each dependency chart. *)
-
- "\n"^
- "
"^headline^"
\n\n"^notice1^notice2^back^
- "\n"^""^th^"\n"^
- (if suffix="sup"
- then ("\n\n")
- else ("\n\n"))^
- "\n");
-
- (* Recursively call the function dependencies *)
- (* to create an entry in the chart for all the *)
- (* levels of dependencies in the hierarchical *)
- (* structure of theory files for a given *)
- (* theory. *)
-
- output(outf_each,
- join(dependencies(th,theorymatrix),""));
-
- output(outf_each,
- "
\n"^bottom);
-
- (* Close for output the individual *)
- (* dependency charts. *)
-
- close_out (outf_each)
- end;
- in
-
- (* Anti-bugging technique to follow the *)
- (* execution of the program. *)
-
- output(std_out,"theory: "^th^"\n");
-
-
- (* The main driver for the creation of the dependencies *)
- (* which calls the functions page and pages. This will *)
- (* go into depth of dependency of each theory with the *)
- (* appropriate indentation. *)
-
- page(th);
- pages(theories,theorymatrix,suffix,headline)
- end;
-
-
-
-
-(* ---------------------------------------------------------------------- *)
-
-
-
-
-(* --------------------
- Generate the main chart 00-chart.html containing
- the listing of all the theories and the links to charts.
- -------------------- *)
-
-val outtext = htmlpath^"00-chart.html";
-val outfile = open_out outtext;
-
-val head = "\n\n"^outtext^
- "\n\n\n"^"\n";
-
-val title = "Dependency Diagram
\n\n"^notice1^notice2;
-val page1part1 = "Subtheories and Supertheories
\n
\n\n"^
- join(all_list(theories),"")^"
\n";
-val page1part3 = bottom;
-
-val tail = "\n"^"";
-
-output(outfile,head);
-output(outfile,title);
-output(outfile,page1part1);
-output(outfile,page1part3);
-
-
-
-(* ---------------------------------------------------------------------- *)
-
-
-
-(* --------------------
- The main driver to create individual super- and sub-theory
- charts for each individual theory. The arguments passed are:
- - the list of all the theories
- - the super- or sub-theory matrix
- - the appropriate suffix sup or sub
- - the title of the chart
- It calls the function:
- - pages
- -------------------- *)
-
-pages(theories,subtheories,"sub","Subtheories");
-pages(theories,supertheories,"sup","Supertheories");
-output(outfile,tail);
-
-
-
-(* --------------------
- Close file for output.
- -------------------- *)
-close_out(outfile);
diff -r ee8f41456d28 -r e173be970d27 src/Pure/Thy/red_arrow.gif
Binary file src/Pure/Thy/red_arrow.gif has changed
diff -r ee8f41456d28 -r e173be970d27 src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML Tue Oct 24 13:41:06 1995 +0100
+++ b/src/Pure/Thy/thy_read.ML Tue Oct 24 13:53:09 1995 +0100
@@ -9,14 +9,13 @@
*)
(*Type for theory storage*)
-datatype thy_info = ThyInfo of {path: string,
- children: string list,
- thy_time: string option,
- ml_time: string option,
- theory: theory option,
- thms: thm Symtab.table,
- thy_ss: Simplifier.simpset option,
- simpset: Simplifier.simpset option};
+datatype thy_info =
+ ThyInfo of {path: string,
+ children: string list, parents: string list,
+ thy_time: string option, ml_time: string option,
+ theory: theory option, thms: thm Symtab.table,
+ thy_ss: Simplifier.simpset option,
+ simpset: Simplifier.simpset option};
(*meaning of special values:
thy_time, ml_time = None theory file has not been read yet
= Some "" theory was read but has either been marked
@@ -24,6 +23,15 @@
this theory (see e.g. 'virtual' theories
like Pure or theories without a ML file)
theory = None theory has not been read yet
+
+ parents: While 'children' contains all theories the theory depends
+ on (i.e. also ones quoted in the .thy file),
+ 'parents' only contains the theories which were used to form
+ the base of this theory.
+
+ origin of the simpsets:
+ thy_ss: snapshot of !Simpset.simpset after .thy file was read
+ simpset: snapshot of !Simpset.simpset after .ML file was read
*)
signature READTHY =
@@ -44,6 +52,9 @@
val theory_of_sign: Sign.sg -> theory
val theory_of_thm: thm -> theory
+ val children_of: string -> string list
+ val parents_of: string -> string list
+
val store_thm: string * thm -> thm
val bind_thm: string * thm -> unit
val qed: string -> unit
@@ -55,6 +66,12 @@
val thms_of: theory -> (string * thm) list
val simpset_of: string -> Simplifier.simpset
val print_theory: theory -> unit
+
+ val gif_path : string ref
+ val chart00_path : string ref
+ val make_html : bool ref
+ val init_html: unit -> unit
+ val make_chart: unit -> unit
end;
@@ -66,29 +83,52 @@
datatype basetype = Thy of string
| File of string;
-val loaded_thys = ref (Symtab.make [("ProtoPure",
- ThyInfo {path = "",
- children = ["Pure", "CPure"],
- thy_time = Some "", ml_time = Some "",
- theory = Some proto_pure_thy,
- thms = Symtab.null,
- thy_ss = None, simpset = None}),
- ("Pure", ThyInfo {path = "", children = [],
- thy_time = Some "", ml_time = Some "",
- theory = Some pure_thy,
- thms = Symtab.null,
- thy_ss = None, simpset = None}),
- ("CPure", ThyInfo {path = "",
- children = [],
- thy_time = Some "", ml_time = Some "",
- theory = Some cpure_thy,
- thms = Symtab.null,
- thy_ss = None, simpset = None})
- ]);
+val loaded_thys =
+ ref (Symtab.make [("ProtoPure",
+ ThyInfo {path = "",
+ children = ["Pure", "CPure"], parents = [],
+ thy_time = Some "", ml_time = Some "",
+ theory = Some proto_pure_thy, thms = Symtab.null,
+ thy_ss = None, simpset = None}),
+ ("Pure",
+ ThyInfo {path = "", children = [],
+ parents = ["ProtoPure"],
+ thy_time = Some "", ml_time = Some "",
+ theory = Some pure_thy, thms = Symtab.null,
+ thy_ss = None, simpset = None}),
+ ("CPure",
+ ThyInfo {path = "",
+ children = [], parents = ["ProtoPure"],
+ thy_time = Some "", ml_time = Some "",
+ theory = Some cpure_thy,
+ thms = Symtab.null,
+ thy_ss = None, simpset = None})
+ ]);
-val loadpath = ref ["."]; (*default search path for theory files *)
+val loadpath = ref ["."]; (*default search path for theory files*)
+
+val delete_tmpfiles = ref true; (*remove temporary files after use*)
+
-val delete_tmpfiles = ref true; (*remove temporary files after use *)
+(*Set location of graphics for HTML files
+ (When this is executed for the first time we are in $ISABELLE/Pure/Thy.
+ This path is converted to $ISABELLE/Tools by removing the last two
+ directories and appending "Tools". All subsequently made ReadThy
+ structures inherit this value.)
+*)
+val gif_path = ref (tack_on ("/" ^
+ space_implode "/" (rev (tl (tl (rev (space_explode "/" (pwd ())))))))
+ "Tools");
+
+(*Location of theory-list.txt and 00-chart.html (normally set by init_html)*)
+val chart00_path = ref "";
+
+val make_html = ref false; (*don't make HTML versions of loaded theories*)
+
+(*HTML file of theory currently being read
+ (Initialized by thyfile2html; used by use_thy and store_thm)*)
+val cur_htmlfile = ref None : outstream option ref;
+
(*Make name of the output ML file for a theory *)
fun out_name tname = "." ^ tname ^ ".thy.ML";
@@ -136,38 +176,42 @@
end
| None => (false, false)
+(*Get all direct descendants of a theory*)
+fun children_of t =
+ case get_thyinfo t of Some (ThyInfo {children, ...}) => children
+ | _ => [];
+
(*Get all direct ancestors of a theory*)
-fun get_parents child =
- let fun has_child (tname, ThyInfo {children, theory, ...}) =
- if child mem children then Some tname else None;
- in mapfilter has_child (Symtab.dest (!loaded_thys)) end;
+fun parents_of t =
+ case get_thyinfo t of Some (ThyInfo {parents, ...}) => parents
+ | _ => [];
(*Get all descendants of a theory list *)
fun get_descendants [] = []
| get_descendants (t :: ts) =
- let val tinfo = get_thyinfo t
- in if is_some tinfo then
- let val ThyInfo {children, ...} = the tinfo
- in children union (get_descendants (children union ts))
- end
- else []
- end;
+ let val children = children_of t
+ in children union (get_descendants (children union ts)) end;
(*Get theory object for a loaded theory *)
-fun get_theory name =
+fun theory_of name =
let val ThyInfo {theory, ...} = the (get_thyinfo name)
in the theory end;
+(*Get path where theory's files are located*)
+fun path_of tname =
+ let val ThyInfo {path, ...} = the (get_thyinfo tname)
+ in path end;
+
exception FILE_NOT_FOUND; (*raised by find_file *)
(*Find a file using a list of paths if no absolute or relative path is
specified.*)
fun find_file "" name =
- let fun find_it (curr :: paths) =
- if file_exists (tack_on curr name) then
- tack_on curr name
+ let fun find_it (cur :: paths) =
+ if file_exists (tack_on cur name) then
+ (if cur = "." then name else tack_on cur name)
else
- find_it paths
+ find_it paths
| find_it [] = ""
in find_it (!loadpath) end
| find_file path name =
@@ -219,9 +263,9 @@
(*Remove theory from all child lists in loaded_thys *)
fun unlink_thy tname =
- let fun remove (ThyInfo {path, children, thy_time, ml_time, theory, thms,
- thy_ss, simpset}) =
- ThyInfo {path = path, children = children \ tname,
+ let fun remove (ThyInfo {path, children, parents, thy_time, ml_time,
+ theory, thms, thy_ss, simpset}) =
+ ThyInfo {path = path, children = children \ tname, parents = parents,
thy_time = thy_time, ml_time = ml_time, theory = theory,
thms = thms, thy_ss = thy_ss, simpset = simpset}
in loaded_thys := Symtab.map remove (!loaded_thys) end;
@@ -234,15 +278,13 @@
(*Change thy_time and ml_time for an existent item *)
fun set_info tname thy_time ml_time =
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
- Some (ThyInfo {path, children, theory, thms, thy_ss, simpset,...}) =>
- ThyInfo {path = path, children = children,
+ Some (ThyInfo {path, children, parents, theory, thms,
+ thy_ss, simpset,...}) =>
+ ThyInfo {path = path, children = children, parents = parents,
thy_time = thy_time, ml_time = ml_time,
theory = theory, thms = thms,
thy_ss = thy_ss, simpset = simpset}
- | None => ThyInfo {path = "", children = [],
- thy_time = thy_time, ml_time = ml_time,
- theory = None, thms = Symtab.null,
- thy_ss = None, simpset = None};
+ | None => error ("set_info: theory " ^ tname ^ " not found");
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
end;
@@ -250,14 +292,205 @@
fun mark_outdated tname =
let val t = get_thyinfo tname;
in if is_none t then ()
- else let val ThyInfo {thy_time, ml_time, ...} = the t
- in set_info tname
- (if is_none thy_time then None else Some "")
- (if is_none ml_time then None else Some "")
-
- end
+ else
+ let val ThyInfo {thy_time, ml_time, ...} = the t
+ in set_info tname (if is_none thy_time then None else Some "")
+ (if is_none ml_time then None else Some "")
+ end
end;
+(*Make head of HTML dependency charts
+ Parameters are:
+ file: HTML file
+ tname: theory name
+ suffix: suffix of complementary chart
+ (sup if this head is for a sub-chart, sub if it is for a sup-chart;
+ empty for Pure and CPure sub-charts)
+ gif_path: relative path to directory containing GIFs
+ chart00_path: relative path to directory containing main theory chart
+*)
+fun mk_charthead file tname title green_arrow gif_path chart00_path package =
+ output (file,
+ "" ^ title ^ " of " ^ tname ^
+ "\n" ^ title ^ " of theory " ^ tname ^
+ "
\nThe name of every theory is linked to its theory file
\n" ^
+ "![\\/](\"")
stands for subtheories (child theories)
\n\
+ \ stands for supertheories (parent theories)\n" ^
+ (if not green_arrow then "" else
+ "
stands for repeated subtrees") ^
+ "Back to the main theory chart 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 = hd (rev (space_explode "/" (!chart00_path)));
+ val chart00_path = relative_path tpath (!chart00_path);
+
+ (*Make list of all theories and all theories that own a .thy file*)
+ fun list_theories [] theories thy_files = (theories, thy_files)
+ | list_theories ((tname, ThyInfo {thy_time, ...}) :: ts)
+ theories thy_files =
+ list_theories ts (tname :: theories)
+ (if is_some thy_time andalso the thy_time <> "" then
+ tname :: thy_files
+ else thy_files);
+
+ val (theories, thy_files) =
+ list_theories (Symtab.dest (!loaded_thys)) [] [];
+
+ (*Do the conversion*)
+ fun gettext thy_file =
+ let
+ (*Convert special HTML characters ('&', '>', and '<')*)
+ val file =
+ explode (execute ("sed -e 's/\\&/\\&/g' -e 's/>/\\>/g' \
+ \-e 's/" ^ t ^ "" end;
+ in if not (id mem theories) then (result, implode l)
+ else if id mem thy_files then
+ make_links rest (result ^ implode pre ^ make_link id)
+ else make_links rest (result ^ implode pre ^ id)
+ end;
+
+ val (pre, rest) = take_prefix (fn c => c <> "=") file';
+
+ val (ancestors, body) =
+ if null rest then
+ error ("Missing \"=\" in file " ^ tname ^ ".thy.\n\
+ \(Make sure that the last line ends with a linebreak.)")
+ else
+ make_links rest "";
+ 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
\n"
+ end;
+
+ (** Make chart of super-theories **)
+
+ val sup_out = open_out (tack_on tpath tname ^ "_sup.html");
+ val sub_out = open_out (tack_on tpath tname ^ "_sub.html");
+
+ (*Theories that already have been listed in this chart*)
+ val listed = ref [];
+
+ val wanted_theories =
+ filter (fn s => s mem thy_files orelse s = "Pure" orelse s = "CPure")
+ theories;
+
+ (*Make nested list of theories*)
+ 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 chart00_path
+ else relative_path tpath path;
+
+ fun mk_offset [] cur =
+ if level < cur then error "Error in mk_offset"
+ else implode (replicate (level - cur) " ")
+ | mk_offset (l::ls) cur =
+ implode (replicate (l - cur) " ") ^ "| " ^
+ mk_offset ls (l+1);
+ in output (sup_out,
+ " " ^ mk_offset continued 0 ^
+ "\\__" ^ (if is_pure then t else "" ^ t ^ "") ^
+ " " ^
+ (if is_pure then ""
+ else ""));
+ if t mem (!listed) andalso not (null (parents_of t)) then
+ output (sup_out,
+ "\
+ \\n")
+ else (output (sup_out, "\n");
+ listed := t :: (!listed);
+ list_ancestors t (level+1) (if null ts then continued
+ else continued @ [level]);
+ mk_entry ts)
+ end;
+
+ val relatives =
+ filter (fn s => s mem wanted_theories) (parents_of tname);
+ in mk_entry relatives end;
+ in if is_some (!cur_htmlfile) then
+ error "thyfile2html: Last theory's HTML has not been closed."
+ else ();
+ cur_htmlfile := Some (open_out (tack_on tpath tname ^ ".html"));
+ output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy"));
+
+ mk_charthead sup_out tname "Ancestors" true gif_path chart00_path package;
+ output(sup_out,
+ "" ^ tname ^ " \
+ \\n");
+ list_ancestors tname 0 [];
+ output (sup_out, "
");
+ close_out sup_out;
+
+ mk_charthead sub_out tname "Children" false gif_path chart00_path package;
+ output(sub_out,
+ "" ^ tname ^ " \
+ \\n");
+ close_out sub_out
+ end;
+
+
(*Read .thy and .ML files that haven't been read yet or have changed since
they were last read;
loaded_thys is a thy_info list ref containing all theories that have
@@ -270,14 +503,16 @@
val (abs_path, _) = if thy_file = "" then split_filename ml_file
else split_filename thy_file;
val (thy_uptodate, ml_uptodate) = thy_unchanged tname thy_file ml_file;
+ val old_parents = parents_of tname;
(*Set absolute path for loaded theory *)
fun set_path () =
- let val ThyInfo {children, thy_time, ml_time, theory, thms, thy_ss,
- simpset, ...} =
+ let val ThyInfo {children, parents, thy_time, ml_time, theory, thms,
+ thy_ss, simpset, ...} =
the (Symtab.lookup (!loaded_thys, tname));
in loaded_thys := Symtab.update ((tname,
- ThyInfo {path = abs_path, children = children,
+ ThyInfo {path = abs_path,
+ children = children, parents = parents,
thy_time = thy_time, ml_time = ml_time,
theory = theory, thms = thms,
thy_ss = thy_ss, simpset = simpset}),
@@ -286,7 +521,7 @@
(*Mark all direct descendants of a theory as changed *)
fun mark_children thy =
- let val ThyInfo {children, ...} = the (get_thyinfo thy);
+ let val children = children_of thy;
val present = filter (is_some o get_thyinfo) children;
val loaded = filter already_loaded present;
in if loaded <> [] then
@@ -301,13 +536,13 @@
fun delete_thms () =
let
val tinfo = case get_thyinfo tname of
- Some (ThyInfo {path, children, thy_time, ml_time, theory, thy_ss,
- simpset, ...}) =>
- ThyInfo {path = path, children = children,
+ Some (ThyInfo {path, children, parents, thy_time, ml_time, theory,
+ thy_ss, simpset, ...}) =>
+ ThyInfo {path = path, children = children, parents = parents,
thy_time = thy_time, ml_time = ml_time,
theory = theory, thms = Symtab.null,
thy_ss = thy_ss, simpset = simpset}
- | None => ThyInfo {path = "", children = [],
+ | None => ThyInfo {path = "", children = [], parents = [],
thy_time = None, ml_time = None,
theory = None, thms = Symtab.null,
thy_ss = None, simpset = None};
@@ -320,10 +555,11 @@
end;
fun save_thy_ss () =
- let val ThyInfo {path, children, thy_time, ml_time, theory, thms,
- simpset, ...} = the (get_thyinfo tname);
+ let val ThyInfo {path, children, parents, thy_time, ml_time,
+ theory, thms, simpset, ...} = the (get_thyinfo tname);
in loaded_thys := Symtab.update
- ((tname, ThyInfo {path = path, children = children,
+ ((tname, ThyInfo {path = path,
+ children = children, parents = parents,
thy_time = thy_time, ml_time = ml_time,
theory = theory, thms = thms,
thy_ss = Some (!Simplifier.simpset),
@@ -332,10 +568,11 @@
end;
fun save_simpset () =
- let val ThyInfo {path, children, thy_time, ml_time, theory, thms,
- thy_ss, ...} = the (get_thyinfo tname);
+ let val ThyInfo {path, children, parents, thy_time, ml_time,
+ theory, thms, thy_ss, ...} = the (get_thyinfo tname);
in loaded_thys := Symtab.update
- ((tname, ThyInfo {path = path, children = children,
+ ((tname, ThyInfo {path = path,
+ children = children, parents = parents,
thy_time = thy_time, ml_time = ml_time,
theory = theory, thms = thms,
thy_ss = thy_ss,
@@ -343,22 +580,58 @@
!loaded_thys)
end;
+ (*Add theory to file listing all loaded theories (for 00-chart.html)
+ and to the sub-charts of its parents*)
+ fun mk_html () =
+ let val new_parents = parents_of tname \\ old_parents;
+
+ (*Add child to parents' sub-theory charts*)
+ fun add_to_parents t =
+ let val is_pure = t = "Pure" orelse t = "CPure";
+ val path = if is_pure then (!chart00_path) else path_of t;
+
+ val gif_path = relative_path path (!gif_path);
+ val rel_path = relative_path path abs_path;
+
+ val out = open_append (tack_on path t ^ "_sub.html");
+ in output (out,
+ " |\n \\__" ^
+ tname ^ " \
+ \\
+ \\n");
+ close_out out
+ end;
+
+ val theory_list =
+ open_append (tack_on (!chart00_path) "theory_list.txt");
+ in output (theory_list, tname ^ " " ^ abs_path ^ "\n");
+ close_out theory_list;
+
+ seq add_to_parents new_parents
+ end
in if thy_uptodate andalso ml_uptodate then ()
else
- (
- if thy_file = "" then ()
+ (if thy_file = "" then ()
else if thy_uptodate then
simpset := let val ThyInfo {thy_ss, ...} = the (get_thyinfo tname);
in the thy_ss end
else
(writeln ("Reading \"" ^ name ^ ".thy\"");
+
delete_thms ();
read_thy tname thy_file;
use (out_name tname);
save_thy_ss ();
if not (!delete_tmpfiles) then ()
- else delete_file (out_name tname)
+ else delete_file (out_name tname);
+
+ if not (!make_html) then ()
+ else thyfile2html abs_path tname
);
set_info tname (Some (file_info thy_file)) None;
@@ -375,21 +648,37 @@
(*Store axioms of theory
(but only if it's not a copy of an older theory)*)
- let val parents = get_parents tname;
- val fst_thy = get_theory (hd parents);
- val this_thy = get_theory tname;
+ let val parents = parents_of tname;
+ val this_thy = theory_of tname;
val axioms =
if length parents = 1
- andalso Sign.eq_sg (sign_of fst_thy, sign_of this_thy) then []
+ andalso Sign.eq_sg (sign_of (theory_of (hd parents)),
+ sign_of this_thy) then []
else axioms_of this_thy;
in map store_thm_db axioms end;
+ (*Add theory to list of all loaded theories (for 00-chart.html)
+ and add it to its parents' sub-charts*)
+ if !make_html then
+ let val path = path_of tname;
+ in if path = "" then mk_html () (*first time theory has been read*)
+ else ()
+ end
+ else ();
+
(*Now set the correct info*)
set_info tname (Some (file_info thy_file)) (Some (file_info ml_file));
set_path ();
(*Mark theories that have to be reloaded*)
- mark_children tname
+ mark_children tname;
+
+ (*Close HTML file*)
+ case !cur_htmlfile of
+ Some out => (output (out, "
![(sub)](\""^srcpath^"red_arrow.gif\"){kind=icon}
\n"^
-" stands for subtheories (child theories) ![(super)](\""^srcpath^"blue_arrow.gif\"){kind=icon}
\n"^
-" stands for supertheories (parent theories)