--- a/src/Pure/Thy/chart.ML Tue Oct 24 13:41:06 1995 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,377 +0,0 @@
-(* ID: $Id$
- Author: Mateja Jamnik, University of Cambridge
- Copyright 1995 University of Cambridge
-
- Generator of the dependency charts of Isabelle theories.
-*)
-
-
-(* --------------------
- Declaration of the variables carrying the name
- of the location of source files:
-
- path - location where the generated HTML files
- should be stored
- srcpath - location where the source files are stored
- (ie. the graphics files)
- -------------------- *)
-
-val htmlpath = "/homes/lcp/html_isa/";
-val srcpath = "/homes/lcp/Isa/Theory/";
-
-
-
-(* --------------------
- Notices that display the legend for every dependency
- chart, and the link back to the main listing of all
- theories.
- -------------------- *)
-
-val notice1 =
-"<BR>\n"^"The name of the file is linked to the theory file <BR>\n";
-
-val notice2 =
-"<IMG SRC = \""^srcpath^"red_arrow.gif\" ALT = (sub)></A>\n"^
-" stands for subtheories (child theories) <BR>\n"^
-
-"<IMG SRC = \""^srcpath^"blue_arrow.gif\" ALT = (super)></A>\n"^
-" stands for supertheories (parent theories) <BR>\n<BR>\n";
-
-
-val back = "<A HREF = \""^htmlpath^"00-chart.html\">Back</A>\n"^
-" to the original listing of all the theories. <BR>\n<HR>\n<BR>\n";
-
-
-
-(* --------------------
- Get a list of all theory files in Isabelle
- that have been loaded.
- -------------------- *)
-
-print_depth 1000;
-
-val theory_list = !loaded_thys;
-
-val files = Symtab.alist_of (theory_list);
-
-
-
-(* --------------------
- Get a list of all theory files and their children.
- -------------------- *)
-
-fun subtheory (tname, ThyInfo{children,...}) = (tname,children);
-
-val subtheories = map subtheory (files);
-
-
-
-(* --------------------
- Extract a list of all theory files only.
- -------------------- *)
-
-fun theory ( [], list ) = list
- | theory ( (string, _)::rest, list ) = theory(rest, string::list);
-
-
-
-(* --------------------
- Use quick sort to sort the theories in
- the alphabetic order. Variable a as the first
- element of the list is used as a pivot value.
- -------------------- *)
-
-fun quick [] = []
- | quick [x] = [x]
- | quick (a::bs) = let
- fun part (l,r,[]) : string list = (quick l) @ (a::quick r)
- | part (l,r,x::xs) = if x<=a then part(x::l, r, xs)
- else part(l, x::r, xs)
- in part([], [], bs) end;
-
-val theories = quick(theory(subtheories,[]));
-
-
-
-(* --------------------
- Insert the identifier of the supertheory
- matrix for every row. Also insert elements
- into the list of identifier's parents in
- alphabetic order.
- -------------------- *)
-
-fun listins ( l, [], x:string ) = l@[x]
- | listins ( l, e::r, x ) = if x>e then listins( l@[e], r, x )
- else if x<>e then l@[x,e]@r
- else l@[x]@r;
-
-
-
-(* --------------------
- Arguments:
- t - accumulator of the resulting supertheory matrix
- result - temporary resulting matrix (up until now)
- (e,ident) - a list of identifier and its child
- The child e of subtheory matrix becomes identifier ident of
- the supertheory matrix. The identifier ident of subtheory
- matrix becomes the parent elem of supertheory matrix.
- Call function:
- - listins
- -------------------- *)
-
-fun matins ( t, [], (ident:string, elem:string) ) = t@[(ident,[elem])]
- | matins ( t, (x:string,y:string list)::b,
- (ident:string, elem:string) ) =
- if x=ident then t@[(x,listins([],y,elem))]@b
- else matins (t@[(x,y)], b, (ident,elem));
-
-
-
-(* --------------------
- Instantiate the identifier ident, and the list of
- its children (e::l), where e is its first child.
- Call function:
- - matins
- -------------------- *)
-
-fun rowins ( (ident, []), result ) = result
- | rowins ( (ident, e::l), result ) =
- rowins ( (ident, l), matins([],result,(e,ident)) );
-
-
-
-(* --------------------
- Extract recursively one row at a time of the
- subtheory matrix.
- Call function:
- -rowins
- -------------------- *)
-
-fun matinv ( [], result ) = result
- | matinv ( l::b, result ) = matinv( b, rowins(l, result) );
-
-
-
-(* --------------------
- Holds the value of supertheory matrix.
- Call function:
- -matinv
- -------------------- *)
-
-val supertheories = matinv ( subtheories, [] );
-
-
-
-
-(* ---------------------------------------------------------------------- *)
-
-
-
-
-(* --------------------
- Entries for the main chart of all the theories.
- Every theory name is a link to the theory definition.
- Down arrow is a link to the subtheory chart of that theory.
- Up arrow is a link to the supertheory chart of that theory.
- -------------------- *)
-
-fun entries x = "\n"^
- "<A HREF = \""^htmlpath^x^
- "_sub.html\">\n<IMG SRC = \""^srcpath^
- "red_arrow.gif\" ALT = (sub)></A>\n"^
-
- "<A HREF = \""^htmlpath^x^
- "_sup.html\">\n<IMG SRC = \""^srcpath^
- "blue_arrow.gif\" ALT = (super)></A> \n"^
- "<A HREF = \""^htmlpath^x^".html\">"^x^"</A><BR>\n";
-
-fun all_list x = map entries x;
-
-
-
-(* --------------------
- Convert a list of characters and strings
- into a string.
- -------------------- *)
-
-fun join ([],res) = res
- | join (x::xs,res) = join(xs,res^x);
-
-
-
-val bottom =
-"<HR>\n\n"^
-"<! ---------------------------------------------------------------- >\n\n";
-
-
-
-(* --------------------
- Find the row of the matrix into which
- the parent (or children) theories
- are going to be inserted.
- -------------------- *)
-
-fun findline (_,[]) = []
- | findline (th:string,(id,row:string list)::mat) =
- if th=id then row else findline(th,mat);
-
-
-
-(* --------------------
- Once a parent (or child) theory has been identified
- make an entry for it with appropriate indentation and with
- further links to its parent (or child) dependency chart.
- It contains the subfunction:
- - maketableentry
- -------------------- *)
-
-fun dependencies (th, mat) =
- let
- val stringlist = findline(th,mat);
- fun maketableentry name =
- "<LI> <A HREF=\""^htmlpath^name^".html\">"^name^"</A>\n"^
- " <A HREF = \""^htmlpath^name^
- "_sub.html\">\n<IMG SRC = \""^srcpath^
- "red_arrow.gif\" ALT = (sub)></A> \n"^
- "<A HREF = \""^htmlpath^name^
- "_sup.html\">\n<IMG SRC = \""^srcpath^
- "blue_arrow.gif\" ALT = (super)></A>\n"^
- "<UL>\n"^
- join(dependencies(name,mat),"")^
- "</UL>\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. *)
-
- "<A NAME=\""^th^"_"^suffix^".html\"></a>\n"^
- "<BR><H1>"^headline^"</H1>\n\n"^notice1^notice2^back^
- "\n"^"<A HREF=\""^htmlpath^th^".html\">"^th^"</A>\n"^
- (if suffix="sup"
- then ("<A HREF = \""^htmlpath^th^
- "_sub.html\">\n<IMG SRC = \""^srcpath^
- "red_arrow.gif\" ALT = (sub)></A>\n")
- else ("<A HREF = \""^htmlpath^th^
- "_sup.html\">\n<IMG SRC = \""^srcpath^
- "blue_arrow.gif\" ALT = (super)></A>\n"))^
- "<UL>\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,
- "</UL>\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 = "<HTML>\n<HEAD>\n<TITLE>"^outtext^
- "</TITLE>\n</HEAD>\n\n"^"<BODY>\n";
-
-val title = "<H1>Dependency Diagram</H1></P>\n\n"^notice1^notice2;
-val page1part1 = "<H2>Subtheories and Supertheories</H2>\n<BR>\n\n"^
- join(all_list(theories),"")^"<BR>\n";
-val page1part3 = bottom;
-
-val tail = "</BODY>\n"^"</HTML>";
-
-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);
--- 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,
+ "<HTML><HEAD><TITLE>" ^ title ^ " of " ^ tname ^
+ "</TITLE></HEAD>\n<H2>" ^ title ^ " of theory " ^ tname ^
+ "</H2>\nThe name of every theory is linked to its theory file<BR>\n" ^
+ "<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\
+ \\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\
+ \<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\
+ \\" ALT = /\\></A> stands for supertheories (parent theories)\n" ^
+ (if not green_arrow then "" else
+ "<BR><IMG SRC = \"" ^ tack_on gif_path "green_arrow.gif\
+ \\" ALT = >></A> stands for repeated subtrees") ^
+ "<P><A HREF = \"" ^ tack_on chart00_path "00-chart.html\
+ \\">Back</A> to the main theory chart of " ^ package ^ ".\n<HR>\n<PRE>");
+
+(*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/</\\</g' " ^ thy_file));
+
+ (*Isolate first (possibly nested) comment;
+ skip all leading whitespaces*)
+ val (comment, file') =
+ let fun first_comment ("*" :: ")" :: cs) co 1 = (co ^ "*)", cs)
+ | first_comment ("*" :: ")" :: cs) co d =
+ first_comment cs (co ^ "*)") (d-1)
+ | first_comment ("(" :: "*" :: cs) co d =
+ first_comment cs (co ^ "(*") (d+1)
+ | first_comment (" " :: cs) "" 0 = first_comment cs "" 0
+ | first_comment ("\n" :: cs) "" 0 = first_comment cs "" 0
+ | first_comment ("\t" :: cs) "" 0 = first_comment cs "" 0
+ | first_comment cs "" 0 = ("", cs)
+ | first_comment (c :: cs) co d =
+ first_comment cs (co ^ implode [c]) d
+ | first_comment [] co _ =
+ error ("Unexpected end of file " ^ tname ^ ".thy.");
+ in first_comment file "" 0 end;
+
+ (*Process line defining theory's ancestors;
+ convert valid theory names to links to their HTML file*)
+ val (ancestors, body) =
+ let
+ fun make_links l result =
+ let val (pre, letter) = take_prefix (not o is_letter) l;
+
+ val (id, rest) =
+ take_prefix (is_quasi_letter orf is_digit) letter;
+
+ val id = implode id;
+
+ (*Make a HTML link out of a theory name*)
+ fun make_link t =
+ let val path = path_of t;
+ in "<A HREF = \"" ^
+ tack_on (relative_path tpath path) t ^
+ ".html\">" ^ t ^ "</A>" 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 "<HTML><HEAD><TITLE>" ^ tname ^ ".thy</TITLE></HEAD>\n\n<BODY>\n" ^
+ "<H2>" ^ tname ^ ".thy</H2>\n<A HREF = \"" ^
+ tack_on chart00_path "00-chart.html\
+ \\">Back</A> to the main theory chart of " ^ package ^
+ ".\n<HR>\n\n<PRE>\n" ^ comment ^ ancestors ^ body ^
+ "</PRE>\n<HR><H2>Theorems proved in <A HREF = \"" ^ tname ^
+ ".ML\">" ^ tname ^ ".ML</A>:</H2>\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 "<A HREF=\"" ^
+ tack_on rel_path t ^ ".html\">" ^ t ^ "</A>") ^
+ " <A HREF = \"" ^ tack_on rel_path t ^
+ "_sub.html\"><IMG ALIGN=TOP SRC = \"" ^
+ tack_on gif_path "red_arrow.gif\" ALT = \\/></A>" ^
+ (if is_pure then ""
+ else "<A HREF = \"" ^ tack_on rel_path t ^
+ "_sup.html\"><IMG ALIGN=TOP SRC = \"" ^
+ tack_on gif_path "blue_arrow.gif\
+ \\" ALT = /\\></A>"));
+ if t mem (!listed) andalso not (null (parents_of t)) then
+ output (sup_out,
+ "<A HREF = \"" ^ tack_on rel_path t ^ "_sup.html\">\
+ \<IMG ALIGN=TOP SRC = \"" ^
+ tack_on gif_path "green_arrow.gif\" ALT = >></A>\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,
+ "<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \
+ \<A HREF = \"" ^ tname ^ "_sub.html\"><IMG ALIGN=TOP SRC = \"" ^
+ tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\n");
+ list_ancestors tname 0 [];
+ output (sup_out, "</PRE><HR></BODY></HTML>");
+ close_out sup_out;
+
+ mk_charthead sub_out tname "Children" false gif_path chart00_path package;
+ output(sub_out,
+ "<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \
+ \<A HREF = \"" ^ tname ^ "_sup.html\"><IMG SRC = \"" ^
+ tack_on gif_path "blue_arrow.gif\" ALT = \\/></A>\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 \\__<A HREF=\"" ^ tack_on rel_path tname ^ ".html\">" ^
+ tname ^ "</A> <A HREF = \"" ^
+ tack_on rel_path tname ^
+ "_sub.html\"><IMG ALIGN=TOP SRC = \"" ^
+ tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\
+ \<A HREF = \"" ^ tack_on rel_path tname ^ "_sup.html\">\
+ \<IMG ALIGN=TOP SRC = \"" ^ tack_on gif_path "blue_arrow.gif\
+ \\" ALT = /\\></A>\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, "<HR></BODY></HTML>\n");
+ close_out out;
+ cur_htmlfile := None)
+ | None => ()
)
end;
@@ -405,25 +694,19 @@
let (*List theories in the order they have to be loaded *)
fun load_order [] result = result
| load_order thys result =
- let fun next_level (t :: ts) =
- let val thy = get_thyinfo t
- in if is_some thy then
- let val ThyInfo {children, ...} = the thy
- in children union (next_level ts) end
- else next_level ts
- end
- | next_level [] = [];
+ let fun next_level [] = []
+ | next_level (t :: ts) =
+ let val children = children_of t
+ in children union (next_level ts) end;
- val children = next_level thys;
- in load_order children ((result \\ children) @ children) end;
+ val descendants = next_level thys;
+ in load_order descendants ((result \\ descendants) @ descendants)
+ end;
fun reload_changed (t :: ts) =
- let val thy = get_thyinfo t;
-
- fun abspath () =
- if is_some thy then
- let val ThyInfo {path, ...} = the thy in path end
- else "";
+ let fun abspath () = case get_thyinfo t of
+ Some (ThyInfo {path, ...}) => path
+ | None => "";
val (thy_file, ml_file) = get_filenames (abspath ()) t;
val (thy_uptodate, ml_uptodate) =
@@ -453,7 +736,7 @@
(*Merge theories to build a base for a new theory.
Base members are only loaded if they are missing.*)
fun mk_base bases child mk_draft =
- let (*Show the cycle that would be created by add_child *)
+ let (*Show the cycle that would be created by add_child*)
fun show_cycle base =
let fun find_it result curr =
let val tinfo = get_thyinfo curr
@@ -468,22 +751,23 @@
end
in find_it "" child end;
- (*Check if a cycle would be created by add_child *)
+ (*Check if a cycle would be created by add_child*)
fun find_cycle base =
if base mem (get_descendants [child]) then show_cycle base
else ();
- (*Add child to child list of base *)
+ (*Add child to child list of base*)
fun add_child base =
let val tinfo =
case Symtab.lookup (!loaded_thys, base) of
- Some (ThyInfo {path, children, thy_time, ml_time,
+ Some (ThyInfo {path, children, parents, thy_time, ml_time,
theory, thms, thy_ss, simpset}) =>
- ThyInfo {path = path, children = child ins children,
+ ThyInfo {path = path,
+ children = child ins 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 = [child],
+ | None => ThyInfo {path = "", children = [child], parents = [],
thy_time = None, ml_time = None,
theory = None, thms = Symtab.null,
thy_ss = None, simpset = None};
@@ -516,7 +800,7 @@
(*Load all needed files and make a list of all real theories *)
fun load_base (Thy b :: bs) =
(load b;
- b :: (load_base bs))
+ b :: load_base bs)
| load_base (File b :: bs) =
(load b;
load_base bs) (*don't add it to mergelist *)
@@ -525,26 +809,34 @@
val dummy = unlink_thy child;
val mergelist = load_base bases;
+ val dummy =
+ let val tinfo = case Symtab.lookup (!loaded_thys, child) of
+ Some (ThyInfo {path, children, thy_time, ml_time, theory, thms,
+ thy_ss, simpset, ...}) =>
+ ThyInfo {path = path,
+ children = children, parents = mergelist,
+ thy_time = thy_time, ml_time = ml_time,
+ theory = theory, thms = thms,
+ thy_ss = thy_ss, simpset = simpset}
+ | None => error ("set_parents: theory " ^ child ^ " not found");
+ in loaded_thys := Symtab.update ((child, tinfo), !loaded_thys) end;
+
val base_thy = (writeln ("Loading theory " ^ (quote child));
- merge_thy_list mk_draft (map get_theory mergelist));
+ merge_thy_list mk_draft (map theory_of mergelist));
in simpset := foldr merge_ss (mapfilter get_simpset mergelist, empty_ss);
base_thy
end;
-(*Change theory object for an existent item of loaded_thys
- or create a new item*)
+(*Change theory object for an existent item of loaded_thys*)
fun store_theory (thy, tname) =
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
- Some (ThyInfo {path, children, thy_time, ml_time, thms,
+ Some (ThyInfo {path, children, parents, thy_time, ml_time, thms,
thy_ss, simpset, ...}) =>
- ThyInfo {path = path, children = children,
+ ThyInfo {path = path, children = children, parents = parents,
thy_time = thy_time, ml_time = ml_time,
theory = Some thy, thms = thms,
thy_ss = thy_ss, simpset = simpset}
- | None => ThyInfo {path = "", children = [],
- thy_time = None, ml_time = None,
- theory = Some thy, thms = Symtab.null,
- thy_ss = None, simpset = None};
+ | None => error ("store_theory: theory " ^ tname ^ " not found");
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
end;
@@ -583,11 +875,12 @@
(* Store theorems *)
-(*Store a theorem in the thy_info of its theory*)
+(*Store a theorem in the thy_info of its theory,
+ and in the theory's HTML file*)
fun store_thm (name, thm) =
let
- val (thy_name, ThyInfo {path, children, thy_time, ml_time, theory, thms,
- thy_ss, simpset}) =
+ val (thy_name, ThyInfo {path, children, parents, thy_time, ml_time,
+ theory, thms, thy_ss, simpset}) =
thyinfo_of_sign (#sign (rep_thm thm));
val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false)
@@ -598,13 +891,28 @@
(thms, true))
else error ("Duplicate theorem name " ^ quote s
^ " used in theory database"));
+
+ fun thm_to_html () =
+ let fun escape [] = ""
+ | escape ("<"::s) = "<" ^ escape s
+ | escape (">"::s) = ">" ^ escape s
+ | escape ("&"::s) = "&" ^ escape s
+ | escape (c::s) = c ^ escape s;
+ in case !cur_htmlfile of
+ Some out =>
+ output (out, "<EM>" ^ name ^ "</EM>\n<PRE>" ^
+ escape (explode (string_of_thm (freeze thm))) ^
+ "</PRE><P>\n")
+ | None => ()
+ end;
in
loaded_thys := Symtab.update
- ((thy_name, ThyInfo {path = path, children = children,
+ ((thy_name, 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}),
!loaded_thys);
+ thm_to_html ();
if duplicate then thm else store_thm_db (name, thm)
end;
@@ -613,19 +921,24 @@
val qed_thm = ref flexpair_def(*dummy*);
fun bind_thm (name, thm) =
- (qed_thm := standard thm;
- use_string ["val " ^name^ " = store_thm (" ^quote name^", !qed_thm);"]);
+ (qed_thm := standard thm;
+ store_thm (name, standard thm);
+ use_string ["val " ^ name ^ " = !qed_thm;"]);
fun qed name =
- use_string ["val " ^ name ^ " = store_thm (" ^ quote name ^ ", result ());"];
+ (qed_thm := result ();
+ store_thm (name, !qed_thm);
+ use_string ["val " ^ name ^ " = !qed_thm;"]);
fun qed_goal name thy agoal tacsf =
- (qed_thm := prove_goal thy agoal tacsf;
- use_string ["val " ^ name ^ " = store_thm (" ^ quote name ^", !qed_thm);"]);
+ (qed_thm := prove_goal thy agoal tacsf;
+ store_thm (name, !qed_thm);
+ use_string ["val " ^ name ^ " = !qed_thm;"]);
fun qed_goalw name thy rths agoal tacsf =
- (qed_thm := prove_goalw thy rths agoal tacsf;
- use_string ["val " ^ name ^ " = store_thm (" ^ quote name ^", !qed_thm);"]);
+ (qed_thm := prove_goalw thy rths agoal tacsf;
+ store_thm (name, !qed_thm);
+ use_string ["val " ^ name ^ " = !qed_thm;"]);
(* Retrieve theorems *)
@@ -648,7 +961,7 @@
| get (t::ts) ng searched =
(case Symtab.lookup (thmtab_of_name t, name) of
Some thm => thm
- | None => get ts (ng union (get_parents t)) (t::searched));
+ | None => get ts (ng union (parents_of t)) (t::searched));
val (tname, _) = thyinfo_of_sign (sign_of thy);
in get [tname] [] [] end;
@@ -677,4 +990,89 @@
fun print_theory thy = (Drule.print_theory thy; print_thms thy);
+
+(* Misc HTML functions *)
+
+(*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";
+ 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 ())));
+ in make_html := true;
+ chart00_path := pwd();
+ writeln ("Setting path for 00-chart.html to " ^ quote (!chart00_path) ^
+ "\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
+ end;
+
+(*Generate 00-chart.html*)
+fun make_chart () = if not (!make_html) then () else
+ let val theory_list = open_in (tack_on (!chart00_path) "theory_list.txt");
+ 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 gif_path = relative_path (!chart00_path) (!gif_path);
+
+ (*Make entry for main chart of all theories.*)
+ fun main_entries [] curdir =
+ implode (replicate (length curdir -1) "</UL>\n")
+ | main_entries (t::ts) curdir =
+ let
+ val (name, path) = take_prefix (not_equal " ") (explode t);
+
+ val tname = implode name
+ val tpath =
+ tack_on (relative_path (!chart00_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 "<UL>\n"
+ else if level_diff < 0 then
+ replicate (~level_diff) "</UL>\n"
+ else []) ^
+ "<H3>" ^ space_implode "/" subdir ^ "</H3>\n")
+ else "") ^
+ "<A HREF = \"" ^ tpath ^ "_sub.html\"><IMG SRC = \"" ^
+ tack_on gif_path "red_arrow.gif\" ALT = \\/></A>" ^
+ "<A HREF = \"" ^ tpath ^ "_sup.html\"><IMG SRC = \"" ^
+ tack_on gif_path "blue_arrow.gif\
+ \\" ALT = /\\></A> <A HREF = \"" ^ tpath ^
+ ".html\">" ^ tname ^ "</A><BR>\n" ^
+ main_entries ts subdir
+ end;
+
+ val out = open_out (tack_on (!chart00_path) "00-chart.html");
+ val subdir = relative_path base_path (!chart00_path);
+ in output (out,
+ "<HTML><HEAD><TITLE>Isabelle/" ^ subdir ^ "</TITLE></HEAD>\n\
+ \<H2>Isabelle/" ^ subdir ^ "</H2>\n\
+ \The name of every theory is linked to its theory file<BR>\n\
+ \<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\
+ \\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\
+ \<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\
+ \\" ALT = /\\></A> stands for supertheories (parent theories)\n\
+ \<P><A HREF = \"" ^
+ tack_on (relative_path (!chart00_path) base_path) "logics.html\">\
+ \Back</A> to the index of Isabelle logics.\n<HR>" ^
+ main_entries theories (space_explode "/" base_path) ^
+ "</BODY></HTML>\n");
+ close_out out
+ end;
end;
