--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/chart.ML Fri Aug 11 12:36:15 1995 +0200
@@ -0,0 +1,377 @@
+(* 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);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/to_html.ML Fri Aug 11 12:36:15 1995 +0200
@@ -0,0 +1,273 @@
+(* ID: $Id$
+ Author: Mateja Jamnik, University of Cambridge
+ Copyright 1995 University of Cambridge
+
+ Convert the Isabelle theory files to .html format for hypertext browsing
+*)
+
+val htmlpath = "/homes/lcp/html_isa/";
+
+(* --------------------
+ Exception declaration in case that there is a lexical
+ error occurs.
+ -------------------- *)
+
+exception lex_err;
+
+(* --------------------
+ Get the list of all the theory files and the
+ path to access them in their directories
+ -------------------- *)
+
+print_depth 1000;
+val theory_list = !loaded_thys;
+val files = Symtab.alist_of (theory_list);
+
+(* --------------------
+ The function move_eachf is going to move all the theory
+ files in isabelle to their html format. It takes
+ for arguments the name of the theory (tname) and
+ other theory information such as path (path), theorems (thms)
+ proved, ... It is the main driver of the program, and basically
+ contains all other functions. It contains the following
+ subfunctions:
+ - create_pure
+ - gettext
+ - move_onef
+ - transform
+ -------------------- *)
+
+fun move_eachf (tname, ThyInfo{path,thms,...}) =
+ let val intext = path^tname^".thy";
+ val outtext = htmlpath^tname^".html";
+
+(* --------------------
+ The function gettext takes an instrem from the auxilliary
+ file .thy whose name and path are specified in the existent
+ Isabelle structure, treats the inputted string with all the
+ necessary modifications for html format and puts it into the
+ file with the same name but .html extension. The subfunctions
+ it contains are:
+ - after_first_c
+ - filter
+ - first_comment
+ - format_link
+ - getstring
+ - get_word
+ - he
+ - html
+ - html_escape
+ - insert_link
+ - leading_comment
+ - lc_exists
+ - modify_body
+ - remove_lc
+ - rest
+ - thy_name
+ -------------------- *)
+
+ fun gettext is =
+ let
+ val head = "<HTML>\n<HEAD>\n<TITLE>"^intext^
+ "</TITLE>\n</HEAD>\n\n"^"<BODY>\n";
+ val title = "<H1>"^tname^".thy"^"</H1></P>\n\n"^
+ "<BR>\n<A HREF = \""^htmlpath^
+ "00-chart.html\">Dependency Chart</A>\n"^
+ ": display of dependencies between the theories.\n"^
+ "<BR>\n<HR>\n\n<PRE>\n";
+ val tail = "</PRE>"^"</BODY>\n"^"</HTML>";
+
+
+ (* --------------------
+ The function he (html escape) is going to take
+ every single characterof the input stream and check
+ for ">", "<" and "&" characters that have a special
+ meaning in html and convert them into their corresponding
+ escape sequences.
+ -------------------- *)
+ fun he [] r = r
+ | he ("<"::sl) r = he sl (r@["&","l","t"])
+ | he (">"::sl) r = he sl (r@["&","g","t"])
+ | he ("&"::sl) r = he sl (r@["&","a","m","p"])
+ | he (c::sl) r = he sl (r@[c]);
+
+ fun html_escape sl = he sl [];
+
+ (* --------------------
+ The function first_comment is a pattern checking for
+ nested comments. The argument d will keep track of how
+ deep we are in the nested comment. The function will
+ return the first comment extracted from the input stream,
+ so that we can copy it into the output stream. Lexical
+ error is raised if we open an empty file to read from.
+ -------------------- *)
+ fun first_comment ("*"::")"::cs) co 1 = co@["*",")"]
+ | first_comment ("*"::")"::cs) co d =
+ first_comment cs (co@["*",")"]) (d-1)
+ | first_comment ("("::"*"::cs) co d =
+ first_comment cs (co@["(","*"]) (d+1)
+ | first_comment (c::cs) co d =
+ if d>0 then first_comment cs (co@[c]) d
+ else first_comment cs co d
+ | first_comment [] _ _ = raise lex_err;
+
+ (* --------------------
+ The function lc_exists leading comment exists?)
+ checks whether in the input file at the very beginning
+ there is a comment, which needs to be extracted and put
+ into the output file. We also need to check whether there
+ might be a space, a new line or a tab, which do not
+ exclude the possibility that there is a leading comment.
+ The function returns a boolean value.
+ -------------------- *)
+ fun lc_exists ("("::"*"::_) = true
+ | lc_exists (" "::cs) = lc_exists cs
+ | lc_exists ("\n"::cs) = lc_exists cs
+ | lc_exists ("\t"::cs) = lc_exists cs
+ | lc_exists _ = false;
+
+ (* --------------------
+ In the case that there is a leading comment, this
+ function leading_comment extracts it> It also need
+ to check for any html escape sequences in the comment.
+ -------------------- *)
+ fun leading_comment sl =
+ if (lc_exists sl) then
+ (html_escape (first_comment sl [] 0))
+ else
+ [""];
+
+ (* --------------------
+ The function thy_name checks for the parent theory
+ names apearing after the leading comment. The function
+ returns a boolean value indicating if the word is a
+ theory name, so that a link can be inserted and can look
+ for another potential theory name. If the word is not a
+ theory name then continue to modify the rest of the body.
+ -------------------- *)
+ fun thy_name word =
+ is_some (Symtab.lookup (theory_list, word));
+
+ (* --------------------
+ Creates the right html format when inserting the link.
+ -------------------- *)
+ fun format_link s =
+ let in
+ output(std_out,"\n"^s);
+ "<A HREF = \""^htmlpath^s^".html\">"^s^"</A>"
+ end;
+
+ (* --------------------
+ -------------------- *)
+
+ fun insert_link w = (explode (format_link (implode w)))
+ (* --------------------
+ -------------------- *)
+
+ fun html ( " "::l) r = html l (r@[ " "])
+ | html ( "+"::l) r = html l (r@[ "+"])
+ | html ("\n"::l) r = html l (r@["\n"])
+ | html ("\t"::l) r = html l (r@["\t"])
+ | html l r = r@(get_word l [])
+ (* --------------------
+ -------------------- *)
+ and get_word ( " "::l) w =
+ if (thy_name (implode w))
+ then (insert_link w)@[ " "]@(html l [])
+ else w@[" "]@(html_escape l)
+ | get_word ( "+"::l) w =
+ if (thy_name (implode w))
+ then (insert_link w)@[ "+"]@(html l [])
+ else w@["+"]@(html_escape l)
+ | get_word ("\n"::l) w =
+ if (thy_name (implode w))
+ then (insert_link w)@[ "\n"]@(html l [])
+ else w@["\n"]@(html_escape l)
+ | get_word ("\t"::l) w =
+ if (thy_name (implode w))
+ then (insert_link w)@[ "\t"]@(html l [])
+ else w@["\t"]@(html_escape l)
+ | get_word (c::l) w = (get_word l (w@[c]))
+ | get_word [] [] = []
+ | get_word [] w =
+ if (thy_name (implode w))
+ then (insert_link w)
+ else w;
+
+ (* --------------------
+ -------------------- *)
+ fun modify_body ("="::l) r = r@["="]@(html l [])
+ | modify_body (c::l) r = modify_body l (r@[c])
+ | modify_body [] r = r;
+
+ (* --------------------
+ -------------------- *)
+ fun after_first_c ("*"::")"::cs) 1 = cs
+ | after_first_c ("*"::")"::cs) d = after_first_c cs (d-1)
+ | after_first_c ("("::"*"::cs) d = after_first_c cs (d+1)
+ | after_first_c (c::cs) d = after_first_c cs d
+ | after_first_c cs 0 = cs
+ | after_first_c [] _ = raise lex_err;
+
+ (* --------------------
+ -------------------- *)
+ fun remove_lc sl =
+ if (lc_exists sl) then (after_first_c sl 0) else sl;
+
+ (* --------------------
+ -------------------- *)
+ fun rest sl = modify_body (remove_lc sl) [];
+
+ (* --------------------
+ -------------------- *)
+ fun filter sl = (leading_comment sl) @ (rest sl);
+
+ (* --------------------
+ -------------------- *)
+ fun getstring s =
+ case input (is, 1) of
+ "" => head^title^(implode(filter(explode(s))))^tail
+ | "\n" => getstring (s^"\n")
+ | c => getstring (s^c)
+ in
+ getstring ""
+ end;
+
+ (* --------------------
+ -------------------- *)
+ fun transform t =
+ let
+ val infile = open_in intext;
+ val outfile = open_out outtext
+ in
+ output(std_out,"\nTheory: "^t);
+ output (outfile, gettext(infile));
+ close_in (infile);
+ close_out (outfile)
+ end;
+
+ (* --------------------
+ -------------------- *)
+ fun create_pure p =
+ let
+ val outfile = open_out outtext
+ in
+ output(std_out, "\nCreating Pure.html ...");
+ output (outfile, "<HTML>\n<HEAD>\n<TITLE>"^intext^
+ "</TITLE>\n</HEAD>\n\n"^"<BODY>\n"^
+ "<H1>"^tname^".thy"^"</H1></P>\n\n"^"<PRE>\n"^
+ "This is a theory file called Pure.\n"^
+ "Its children are all other Isabelle theories."^
+ "</PRE>"^"</BODY>\n"^"</HTML>");
+ close_out (outfile)
+ end
+
+ in
+ if (tname <> "Pure") then (transform tname)
+ else (create_pure tname)
+ end;
+
+(* --------------------
+ -------------------- *)
+map move_eachf (files);
+
