--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/browser_info.ML Wed Aug 06 00:24:49 1997 +0200
@@ -0,0 +1,787 @@
+(* Title: Pure/Thy/thy_browser_info.ML
+ ID: $Id$
+ Author: Stefan Berghofer and Carsten Clasohm
+ Copyright 1994, 1997 TU Muenchen
+
+Functions for generating theory browsing information
+(i.e. *.html and *.graph - files).
+*)
+
+signature BROWSER_INFO =
+sig
+ val output_dir : string ref
+ val home_path : string ref
+
+ val make_graph : bool ref
+ val init_graph : string -> unit
+ val mk_graph : string -> string -> unit
+ val cur_thyname : string ref
+ val make_html : bool ref
+ val mk_html : string -> string -> string list -> unit
+ val thyfile2html : string -> string -> unit
+ val init_html : unit -> unit
+ val finish_html : unit -> unit
+ val section : string -> unit
+ val thm_to_html : thm -> string -> unit
+ val close_html : unit -> unit
+end;
+
+
+structure BrowserInfo : BROWSER_INFO =
+struct
+
+open ThyInfo;
+
+
+(*directory where to put html and graph files*)
+val output_dir = ref "";
+
+
+(*path of user home directory*)
+val home_path = ref "";
+
+
+(*normalize a path
+ FIXME: move to library?*)
+fun normalize_path p =
+ let val curr_dir = pwd ();
+ val _ = cd p;
+ val norm_path = pwd ();
+ val _ = cd curr_dir
+ in norm_path end;
+
+
+(*create directory
+ FIXME: move to library?*)
+fun mkdir path = (execute ("mkdir -p " ^ path) ; ());
+
+
+(*Path of Isabelle's main (source) directory
+ FIXME: this value should be provided by isatool!*)
+val base_path = ref (
+ "/" ^ space_implode "/" (rev (tl (tl (rev (space_explode "/" (OS.FileSys.getDir ())))))));
+
+
+(******************** HTML generation functions *************************)
+
+(*Set location of graphics for HTML files*)
+fun gif_path () = tack_on (normalize_path (!output_dir)) "gif";
+
+
+(*Name of theory currently being read*)
+val cur_thyname = ref "";
+
+
+(*Name of current logic*)
+val package = ref "";
+
+
+(* Return path of directory where to store html / graph data
+ corresponding to theory with given path *)
+local
+ fun make_path q p =
+ let val base = tack_on (normalize_path (!output_dir)) q;
+ val rpath = if p subdir_of (!base_path) then relative_path (!base_path) p
+ else relative_path (normalize_path (!home_path)) p;
+ in tack_on base rpath end
+in
+ val html_path = make_path "html";
+ val graph_path = make_path "graph"
+end;
+
+
+(*Location of theory-list.txt and index.html (set by init_html)*)
+val index_path = ref "";
+
+
+(*Original path of ROOT.ML*)
+val original_path = ref "";
+
+
+(*Location of Pure_sub.html and CPure_sub.html*)
+val pure_subchart = ref (None : string option);
+
+
+(*Controls whether HTML files should be generated*)
+val make_html = ref false;
+
+
+(*HTML file of theory currently being read
+ (Initialized by thyfile2html; used by use_thy and store_thm)*)
+val cur_htmlfile = ref None : TextIO.outstream option ref;
+
+
+(*Boolean variable which indicates if the title "Theorems proved in foo.ML"
+ has already been inserted into the current HTML file*)
+val cur_has_title = ref false;
+
+
+(*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
+ index_path: relative path to directory containing main theory chart
+*)
+fun mk_charthead file tname title repeats gif_path index_path package =
+ TextIO.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 repeats then "" else
+ "<BR><TT>...</TT> stands for repeated subtrees") ^
+ "<P>\n<A HREF = \"" ^ tack_on index_path "index.html\
+ \\">Back</A> to the index of " ^ package ^ "\n<HR>\n<PRE>");
+
+
+(*Convert special HTML characters ('&', '>', and '<')*)
+fun escape [] = []
+ | escape ("<"::s) = "<" :: escape s
+ | escape (">"::s) = ">" :: escape s
+ | escape ("&"::s) = "&" :: escape s
+ | escape (c::s) = c :: escape s;
+
+
+(*Convert .thy file to HTML and make chart of its super-theories*)
+fun thyfile2html tname thy_path = if not (!make_html) then () else
+ let
+ (* path of directory, where corresponding HTML file is stored *)
+ val tpath = html_path thy_path;
+
+ (* gif directory *)
+ val rel_gif_path = relative_path tpath (gif_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)
+ | 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)) [] [];
+
+ (*convert ML file to html *)
+ fun ml2html name abs_path =
+ let val is = TextIO.openIn (tack_on abs_path (name ^ ".ML"));
+ val inp = implode (escape (explode (TextIO.inputAll is)));
+ val _ = TextIO.closeIn is;
+ val os = TextIO.openOut (tack_on (html_path abs_path) (name ^ "_ML.html"));
+ val _ = TextIO.output (os,
+ "<HTML><HEAD><TITLE>" ^ name ^ ".ML</TITLE></HEAD>\n\n<BODY>\n" ^
+ "<H2>" ^ name ^ ".ML</H2>\n<A HREF = \"" ^
+ name ^ ".html\">Back</A> to theory " ^ name ^
+ "\n<HR>\n\n<PRE>\n" ^ inp ^ "</PRE><HR></BODY></HTML>");
+ val _ = TextIO.closeOut os;
+ in () end;
+
+ (*Do the conversion*)
+ fun gettext thy_file =
+ let
+ (*Convert special HTML characters ('&', '>', and '<')*)
+ val file =
+ let val is = TextIO.openIn thy_file;
+ val inp = TextIO.inputAll is;
+ in (TextIO.closeIn is; escape (explode inp)) end;
+
+
+ (*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 = html_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 rel_index_path "index.html\
+ \\">Back</A> to the index of " ^ (!package) ^
+ "\n<HR>\n\n<PRE>\n" ^ comment ^ ancestors ^ body ^
+ "</PRE>\n"
+ end;
+
+ (** Make chart of super-theories **)
+
+ val _ = mkdir tpath;
+ val sup_out = TextIO.openOut (tack_on tpath (tname ^ "_sup.html"));
+ val sub_out = TextIO.openOut (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 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 = if is_pure then (the (!pure_subchart))
+ else html_path (path_of t);
+ val rel_path = relative_path tpath path;
+ val repeated = t mem (!listed) andalso
+ not (null (parents_of_name t));
+
+ 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 TextIO.output (sup_out,
+ " " ^ mk_offset continued 0 ^
+ "\\__" ^ (if is_pure then t else
+ "<A HREF=\"" ^ tack_on rel_path t ^
+ ".html\">" ^ t ^ "</A>") ^
+ (if repeated then "..." else " ") ^
+ "<A HREF = \"" ^ tack_on rel_path t ^
+ "_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
+ tack_on rel_gif_path "red_arrow.gif\" ALT = \\/></A>" ^
+ (if is_pure then ""
+ else "<A HREF = \"" ^ tack_on rel_path t ^
+ "_sup.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
+ tack_on rel_gif_path "blue_arrow.gif\
+ \\" ALT = /\\></A>") ^
+ "\n");
+ if repeated then ()
+ else (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_name tname);
+ in mk_entry relatives end;
+ in if is_some (!cur_htmlfile) then
+ (TextIO.closeOut (the (!cur_htmlfile));
+ warning "Last theory's HTML file has not been closed.")
+ else ();
+ cur_htmlfile := Some (TextIO.openOut (tack_on tpath (tname ^ ".html")));
+ cur_has_title := false;
+ if file_exists (tack_on thy_path (tname ^ ".ML"))
+ then ml2html tname thy_path else ();
+ TextIO.output (the (!cur_htmlfile), gettext (tack_on thy_path tname ^ ".thy"));
+
+ mk_charthead sup_out tname "Ancestors" true rel_gif_path rel_index_path
+ (!package);
+ TextIO.output(sup_out,
+ "<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \
+ \<A HREF = \"" ^ tname ^
+ "_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
+ tack_on rel_gif_path "red_arrow.gif\" ALT = \\/></A>\n");
+ list_ancestors tname 0 [];
+ TextIO.output (sup_out, "</PRE><HR></BODY></HTML>");
+ TextIO.closeOut sup_out;
+
+ mk_charthead sub_out tname "Children" false rel_gif_path rel_index_path
+ (!package);
+ TextIO.output(sub_out,
+ "<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \
+ \<A HREF = \"" ^ tname ^ "_sup.html\"><IMG SRC = \"" ^
+ tack_on rel_gif_path "blue_arrow.gif\" BORDER=0 ALT = \\/></A>\n");
+ TextIO.closeOut sub_out
+ end;
+
+
+(*Makes HTML title for list of theorems; as this list may be empty and we
+ don't want a title in that case, mk_theorems_title is only invoked when
+ something is added to the list*)
+fun mk_theorems_title out =
+ if not (!cur_has_title) then
+ (cur_has_title := true;
+ TextIO.output (out, "<HR><H2>Theorems proved in <A HREF = \"" ^
+ (!cur_thyname) ^ "_ML.html\">" ^ (!cur_thyname) ^
+ ".ML</A>:</H2>\n"))
+ else ();
+
+
+exception MK_HTML;
+
+(*Add theory to file listing all loaded theories (for index.html)
+ and to the sub-charts of its parents*)
+fun mk_html tname abs_path old_parents = if not (!make_html) then () else
+ ( let val new_parents = parents_of_name tname \\ old_parents;
+
+ fun robust_seq (proc: 'a -> unit) : 'a list -> unit =
+ let fun seqf [] = ()
+ | seqf (x :: xs) = (proc x handle _ => (); seqf xs)
+ in seqf end;
+
+ (*Add child to parents' sub-theory charts*)
+ fun add_to_parents t =
+ let val path = if t = "Pure" orelse t = "CPure" then
+ (the (!pure_subchart))
+ else html_path (path_of t);
+
+ val rel_gif_path = relative_path path (gif_path ());
+ val rel_path = relative_path path (html_path abs_path);
+ val tpath = tack_on rel_path tname;
+
+ val fname = tack_on path (t ^ "_sub.html");
+ val out = if file_exists fname then
+ TextIO.openAppend fname handle e =>
+ (warning ("Unable to write to file " ^
+ fname); raise e)
+ else raise MK_HTML;
+ in TextIO.output (out,
+ " |\n \\__<A HREF=\"" ^
+ tack_on rel_path tname ^ ".html\">" ^ tname ^
+ "</A> <A HREF = \"" ^ tpath ^ "_sub.html\">\
+ \<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
+ tack_on rel_gif_path "red_arrow.gif\" ALT = \\/></A>\
+ \<A HREF = \"" ^ tpath ^ "_sup.html\">\
+ \<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
+ tack_on rel_gif_path "blue_arrow.gif\" ALT = /\\></A>\n");
+ TextIO.closeOut out
+ end;
+
+ val theory_list =
+ TextIO.openAppend (tack_on (!index_path) "theory_list.txt")
+ handle _ => (make_html := false;
+ warning ("Cannot write to " ^
+ (!index_path) ^ " while making HTML files.\n\
+ \HTML generation has been switched off.\n\
+ \Call init_html() from within a \
+ \writeable directory to reactivate it.");
+ raise MK_HTML)
+ in TextIO.output (theory_list, tname ^ " " ^ abs_path ^ "\n");
+ TextIO.closeOut theory_list;
+ robust_seq add_to_parents new_parents
+ end
+ ) handle MK_HTML => ();
+
+
+(*** Misc HTML functions ***)
+
+(*Init HTML generator by setting paths and creating new files*)
+fun init_html () =
+ let val cwd = OS.FileSys.getDir();
+ val _ = mkdir (html_path cwd);
+
+ val theory_list = TextIO.closeOut (TextIO.openOut (tack_on (html_path cwd) "theory_list.txt"));
+
+ val rel_gif_path = relative_path (html_path cwd) (gif_path ());
+
+ (*Make new HTML files for Pure and CPure*)
+ fun init_pure_html () =
+ let val pure_out = TextIO.openOut (tack_on (html_path cwd) "Pure_sub.html");
+ val cpure_out = TextIO.openOut (tack_on (html_path cwd) "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);
+ TextIO.output (pure_out, "Pure\n");
+ TextIO.output (cpure_out, "CPure\n");
+ TextIO.closeOut pure_out;
+ TextIO.closeOut cpure_out;
+ pure_subchart := Some (html_path cwd)
+ end;
+
+ (*Copy files
+ FIXME: move to library?*)
+ fun copy_file infile outfile = if not (file_exists infile) then () else
+ let val is = TextIO.openIn infile;
+ val inp = TextIO.inputAll is;
+ val _ = TextIO.closeIn is;
+ val os = TextIO.openOut outfile;
+ val _ = TextIO.output (os, inp);
+ val _ = TextIO.closeOut os
+ in () end
+
+ in make_html := true;
+ (*Make sure that base_path contains the physical path and no
+ symbolic links*)
+ base_path := normalize_path (!base_path);
+ original_path := cwd;
+ index_path := html_path cwd;
+ package :=
+ (if cwd subdir_of (!base_path) then
+ relative_path (!base_path) cwd
+ else base_name cwd);
+
+ (*Copy README files to html directory
+ FIXME: let usedir do this job*)
+ copy_file (tack_on cwd "README.html") (tack_on (!index_path) "README.html");
+ copy_file (tack_on cwd "README") (tack_on (!index_path) "README");
+
+ if cwd subdir_of (!base_path) then ()
+ else warning "The current working directory seems to be no \
+ \subdirectory of\nIsabelle's main directory. \
+ \Please ensure that base_path's value is correct.\n";
+
+ writeln ("Setting path for index.html to " ^ quote (!index_path) ^
+ "\nGIF path has been set to " ^ quote (gif_path ()));
+
+ if is_none (!pure_subchart) then init_pure_html()
+ else ()
+ end;
+
+
+(*Generate index.html*)
+fun finish_html () = if not (!make_html) then () else
+ let val tlist_path = tack_on (!index_path) "theory_list.txt";
+ val theory_list = TextIO.openIn tlist_path;
+ val theories = space_explode "\n" (TextIO.inputAll theory_list);
+ val dummy = (TextIO.closeIn theory_list; OS.FileSys.remove tlist_path);
+
+ val rel_gif_path = relative_path (!index_path) (gif_path ());
+
+ (*Make entry for main chart of all theories.*)
+ 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) (html_path (implode (tl path))))
+ tname;
+ in "<A HREF = \"" ^ tpath ^ "_sub.html\"><IMG SRC = \"" ^
+ tack_on rel_gif_path "red_arrow.gif\" BORDER=0 ALT = \\/></A>" ^
+ "<A HREF = \"" ^ tpath ^ "_sup.html\"><IMG SRC = \"" ^
+ tack_on rel_gif_path "blue_arrow.gif\
+ \\" BORDER=0 ALT = /\\></A> <A HREF = \"" ^ tpath ^
+ ".html\">" ^ tname ^ "</A><BR>\n"
+ end;
+
+ val out = TextIO.openOut (tack_on (!index_path) "index.html");
+
+ (*Find out in which subdirectory of Isabelle's main directory the
+ index.html is placed; if original_path is no subdirectory of base_path
+ then take the last directory of index_path*)
+ val inside_isabelle = (!original_path) subdir_of (!base_path);
+ val subdir =
+ if inside_isabelle then relative_path (html_path (!base_path)) (!index_path)
+ else base_name (!index_path);
+ val subdirs = space_explode "/" subdir;
+
+ (*Look for index.html in superdirectories; stop when Isabelle's
+ main directory is reached*)
+ fun find_super_index [] n = ("", n)
+ | 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 if length subdirs - n > 0 then find_super_index ps (n+1)
+ else ("", n)
+ 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 = TextIO.openIn (super_index ^ "/index.html");
+ val content = rev (explode (TextIO.inputAll old_index));
+ val dummy = TextIO.closeIn old_index;
+
+ val out = TextIO.openAppend (super_index ^ "/index.html");
+ val rel_path = space_implode "/" (drop (level, subdirs));
+ in
+ TextIO.output (out,
+ (if nth_elem (3, content) <> "!" then ""
+ else "\n<HR><H3>Subdirectories:</H3>\n") ^
+ "<H3><A HREF = \"" ^ rel_path ^ "/index.html\">" ^ rel_path ^
+ "</A></H3>\n");
+ TextIO.closeOut out
+ end;
+
+ (*If original_path is no subdirectory of base_path then the title should
+ not contain the string "Isabelle/"*)
+ val title = (if inside_isabelle then "Isabelle/" else "") ^ subdir;
+ val rel_graph_path = tack_on (relative_path (!index_path) (graph_path (!original_path)))
+ "theories.html"
+ in TextIO.output (out,
+ "<HTML><HEAD><TITLE>" ^ title ^ "</TITLE></HEAD>\n\
+ \<BODY><H2>" ^ title ^ "</H2>\n\
+ \The name of every theory is linked to its theory file<BR>\n\
+ \<IMG SRC = \"" ^ tack_on rel_gif_path "red_arrow.gif\
+ \\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\
+ \<IMG SRC = \"" ^ tack_on rel_gif_path "blue_arrow.gif\
+ \\" ALT = /\\></A> stands for supertheories (parent theories)<P>\n\
+ \View <A HREF=\"" ^ rel_graph_path ^ "\">graph</A> of theories<P>\n" ^
+ (if super_index = "" then "" else
+ ("<A HREF = \"" ^ relative_path (!index_path) super_index ^
+ "/index.html\">Back</A> to the index of " ^
+ (if not inside_isabelle then
+ hd (tl (rev (space_explode "/" (!index_path))))
+ else if level = 0 then "Isabelle logics"
+ else space_implode "/" (take (level, subdirs))))) ^
+ "\n" ^
+ (if file_exists (tack_on (!index_path) "README.html") then
+ "<BR>View the <A HREF = \"README.html\">ReadMe</A> file.\n"
+ else if file_exists (tack_on (!index_path) "README") then
+ "<BR>View the <A HREF = \"README\">ReadMe</A> file.\n"
+ else "") ^
+ "<HR>" ^ implode (map main_entry theories) ^ "<!-->");
+ TextIO.closeOut out;
+ if super_index = "" orelse (inside_isabelle andalso level = 0) then ()
+ else link_directory ()
+ end;
+
+
+(*Append section heading to HTML file*)
+fun section s =
+ case !cur_htmlfile of
+ Some out => (mk_theorems_title out;
+ TextIO.output (out, "<H3>" ^ s ^ "</H3>\n"))
+ | None => ();
+
+
+(*Add theorem to HTML file*)
+fun thm_to_html thm name =
+ case !cur_htmlfile of
+ Some out =>
+ (mk_theorems_title out;
+ TextIO.output (out, "<DD><EM>" ^ name ^ "</EM>\n<PRE>" ^
+ (implode o escape)
+ (explode
+ (string_of_thm (#1 (freeze_thaw thm)))) ^
+ "</PRE><P>\n")
+ )
+ | None => ();
+
+
+(*Close HTML file*)
+fun close_html () =
+ case !cur_htmlfile of
+ Some out => (TextIO.output (out, "<HR></BODY></HTML>\n");
+ TextIO.closeOut out;
+ cur_htmlfile := None)
+ | None => () ;
+
+
+(******************** Graph generation functions ************************)
+
+
+(*flag that indicates whether graph files should be generated*)
+val make_graph = ref false;
+
+
+(*file to use as basis for new graph files*)
+val graph_base_file = ref "";
+
+
+(*directory containing basic theories (gets label "base")*)
+val graph_root_dir = ref "";
+
+
+(*name of current graph file*)
+val graph_file = ref "";
+
+
+(*name of large graph file which also contains
+ theories defined in subdirectories *)
+val large_graph_file = ref "";
+
+
+(* initialize graph data generator *)
+fun init_graph usedir_arg =
+ let
+ (*create default graph containing only Pure, CPure and ProtoPure*)
+ fun default_graph outfile =
+ let val os = TextIO.openOut outfile;
+ in (TextIO.output(os,"\"ProtoPure\" \"ProtoPure\" \"Pure\" \"\" ;\n\
+ \\"CPure\" \"CPure\" \"Pure\" \"\" > \"ProtoPure\" ;\n\
+ \\"Pure\" \"Pure\" \"Pure\" \"\" > \"ProtoPure\" ;\n");
+ TextIO.closeOut os)
+ end;
+
+ (*copy graph file, adjust relative paths for theory files*)
+ fun copy_graph infile outfile unfold =
+ let val is = TextIO.openIn infile;
+ val (inp_dir, _) = split_filename infile;
+ val (outp_dir, _) = split_filename outfile;
+ val entries = map (space_explode " ")
+ (space_explode "\n" (TextIO.inputAll is));
+
+ fun thyfile f = if f = "\"\"" then f else
+ let val (dir, name) =
+ split_filename (implode (rev (tl (rev (tl (explode f))))));
+ val abs_path = normalize_path (tack_on inp_dir dir);
+ val rel_path = tack_on (relative_path outp_dir abs_path) name
+ in quote rel_path end;
+
+ fun process_entry (a::b::c::d::e::r) =
+ if d = "+" then
+ a::b::c::((if unfold then "+ " else "") ^ (thyfile e))::r
+ else
+ a::b::c::(thyfile d)::e::r;
+
+ val _ = TextIO.closeIn is;
+ val os = TextIO.openOut outfile;
+ val _ = TextIO.output(os, (cat_lines
+ (map ((space_implode " ") o process_entry) entries)) ^ "\n");
+ val _ = TextIO.closeOut os;
+ in () end;
+
+ (*create html page which contains graph browser applet*)
+ fun mk_applet_page abs_path large other_graph =
+ let
+ val dir_name =
+ (if (!original_path) subdir_of (!base_path) then "Isabelle/" else "") ^
+ (relative_path (normalize_path (tack_on (!graph_root_dir) "..")) (pwd ()));
+ val rel_codebase =
+ relative_path abs_path (tack_on (normalize_path (!output_dir)) "graph");
+ val rel_index_path = tack_on (relative_path
+ abs_path (tack_on (normalize_path (!output_dir)) "graph")) "index.html";
+ val outfile =
+ tack_on abs_path ((if large then "all_" else "") ^ "theories.html");
+ val os = TextIO.openOut outfile;
+ val _ = TextIO.output(os,
+ "<HTML><HEAD><TITLE>" ^ dir_name ^ "</TITLE></HEAD>\n\
+ \<BODY><H2>" ^ dir_name ^ "</H2>\n" ^
+ (if other_graph then
+ (if large then
+ "View <A HREF=\"theories.html\">small graph</A> without \
+ \subdirectories<P>\n"
+ else
+ "View <A HREF=\"all_theories.html\">large graph</A> including \
+ \all subdirectories<P>\n")
+ else "") ^
+ "<A HREF=\"" ^ rel_index_path ^ "\">Back</A> to index\n<HR>\n\
+ \<APPLET CODE=\"GraphBrowser/GraphBrowser.class\" \
+ \CODEBASE=\"" ^ rel_codebase ^ "\" WIDTH=550 HEIGHT=450>\n\
+ \<PARAM NAME=\"graphfile\" VALUE=\"" ^
+ (if large then "all_theories.graph" else "theories.graph") ^ "\">\n\
+ \</APPLET>\n<HR>\n</BODY></HTML>")
+ val _ = TextIO.closeOut os
+ in () end;
+
+ val gpath = graph_path (pwd ());
+
+ in
+ (make_graph := true;
+ base_path := normalize_path (!base_path);
+ mkdir gpath;
+ original_path := pwd ();
+ graph_file := tack_on gpath "theories.graph";
+ graph_root_dir := (if usedir_arg = "." then pwd ()
+ else normalize_path (tack_on (pwd ()) ".."));
+ (if (!graph_base_file) = "" then
+ (large_graph_file := tack_on gpath "all_theories.graph";
+ default_graph (!graph_file);
+ default_graph (!large_graph_file);
+ mk_applet_page gpath false true;
+ mk_applet_page gpath true true)
+ else
+ (if (fst (split_filename (!graph_file))) subdir_of
+ (fst (split_filename (!graph_base_file)))
+ then
+ (copy_graph (!graph_base_file) (!graph_file) true;
+ mk_applet_page gpath false false)
+ else
+ (large_graph_file := tack_on gpath "all_theories.graph";
+ mk_applet_page gpath false true;
+ mk_applet_page gpath true true;
+ copy_graph (!graph_base_file) (!graph_file) false;
+ copy_graph (!graph_base_file) (!large_graph_file) false)));
+ graph_base_file := (!graph_file))
+ end;
+
+
+(*add theory to graph definition file*)
+fun mk_graph tname abs_path = if not (!make_graph) then () else
+ let val parents =
+ map (fn (t, _) => tack_on (path_of t) t)
+ (filter (fn (_, ThyInfo {children,...}) => tname mem children)
+ (Symtab.dest(!loaded_thys)));
+
+ val dir_name = relative_path
+ (normalize_path (tack_on (!graph_root_dir) "..")) abs_path;
+
+ val dir_entry = "\"" ^ dir_name ^
+ (if (tack_on abs_path "") = (tack_on (!graph_root_dir) "")
+ then "/base\" + " else "\" ");
+
+ val thy_file = (tack_on (html_path abs_path) tname) ^ ".html";
+
+ val thy_ID = quote (tack_on abs_path tname);
+
+ val entry_str_1 = (quote tname) ^ " " ^ thy_ID ^ " " ^ dir_entry ^
+ (quote (relative_path (fst (split_filename (!graph_file))) thy_file)) ^
+ " > " ^ (space_implode " " (map quote parents)) ^ " ;\n" ;
+
+ val entry_str_2 = (quote tname) ^ " " ^ thy_ID ^ " " ^ dir_entry ^
+ (quote (relative_path (fst (split_filename (!large_graph_file))) thy_file)) ^
+ " > " ^ (space_implode " " (map quote parents)) ^ " ;\n" ;
+
+ fun exists_entry id infile =
+ let val is = TextIO.openIn(infile);
+ val IDs = map (hd o tl o (space_explode " "))
+ (space_explode "\n" (TextIO.inputAll is));
+ val _ = TextIO.closeIn is
+ in id mem IDs end;
+
+ fun mk_entry outfile entry_str =
+ if exists_entry thy_ID outfile then ()
+ else
+ let val os = TextIO.openAppend outfile;
+ val _ = TextIO.output (os, entry_str);
+ val _ = TextIO.closeOut os;
+ in () end
+
+ in (mk_entry (!graph_file) entry_str_1;
+ mk_entry (!large_graph_file) entry_str_2) handle _ =>
+ (make_graph:=false;
+ warning ("Unable to write to graph file " ^ (!graph_file)))
+ end;
+
+end;