isabelle: src/Pure/Thy/browser_info.ML@d59fe4579004 (annotated)

3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	1	(* Title: Pure/Thy/thy_browser_info.ML
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	2	ID: $Id$
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	3	Author: Stefan Berghofer and Carsten Clasohm
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	4	Copyright 1994, 1997 TU Muenchen
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	5
3870 6913700d7c79 Added ack to Mateja Jamnik. nipkow parents: 3868 diff changeset	6	The first design of the text-based html browser is due to Mateja Jamnik.
6913700d7c79 Added ack to Mateja Jamnik. nipkow parents: 3868 diff changeset	7
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	8	Functions for generating theory browsing information
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	9	(i.e. .html and .graph - files).
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	10	*)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	11
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	12	signature BROWSER_INFO =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	13	sig
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	14	val output_dir : string ref
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	15	val home_path : string ref
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	16
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	17	val make_graph : bool ref
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	18	val init_graph : string -> unit
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	19	val mk_graph : string -> string -> unit
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	20	val cur_thyname : string ref
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	21	val make_html : bool ref
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	22	val mk_html : string -> string -> string list -> unit
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	23	val thyfile2html : string -> string -> unit
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	24	val init_html : unit -> unit
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	25	val finish_html : unit -> unit
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	26	val section : string -> unit
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	27	val thm_to_html : thm -> string -> unit
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	28	val close_html : unit -> unit
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	29	end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	30
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	31
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	32	structure BrowserInfo : BROWSER_INFO =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	33	struct
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	34
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	35	open ThyInfo;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	36
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	37
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	38	(directory where to put html and graph files)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	39	val output_dir = ref "";
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	40
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	41
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	42	(path of user home directory)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	43	val home_path = ref "";
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	44
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	45
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	46	(*normalize a path
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	47	FIXME: move to library?*)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	48	fun normalize_path p =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	49	let val curr_dir = pwd ();
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	50	val _ = cd p;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	51	val norm_path = pwd ();
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	52	val _ = cd curr_dir
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	53	in norm_path end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	54
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	55
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	56	(*create directory
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	57	FIXME: move to library?*)
3628 41a49c671901 tuned copy_file; wenzelm parents: 3603 diff changeset	58	fun mkdir path = (execute ("mkdir -p " ^ path); ());
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	59
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	60
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	61	(*Path of Isabelle's main (source) directory
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	62	FIXME: this value should be provided by isatool!*)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	63	val base_path = ref (
3834 278f0a1e5986 BAD_space_explode; wenzelm parents: 3748 diff changeset	64	"/" ^ space_implode "/" (rev (tl (tl (rev (BAD_space_explode "/" (OS.FileSys.getDir ())))))));
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	65
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	66
3628 41a49c671901 tuned copy_file; wenzelm parents: 3603 diff changeset	67	(* copy contents of file ) ( FIXME: move to library?*)
41a49c671901 tuned copy_file; wenzelm parents: 3603 diff changeset	68
41a49c671901 tuned copy_file; wenzelm parents: 3603 diff changeset	69	fun copy_file infile outfile =
41a49c671901 tuned copy_file; wenzelm parents: 3603 diff changeset	70	if not (file_exists infile) then ()
41a49c671901 tuned copy_file; wenzelm parents: 3603 diff changeset	71	else write_file outfile (read_file infile);
41a49c671901 tuned copy_file; wenzelm parents: 3603 diff changeset	72
41a49c671901 tuned copy_file; wenzelm parents: 3603 diff changeset	73
41a49c671901 tuned copy_file; wenzelm parents: 3603 diff changeset	74
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	75	(****************** HTML generation functions ***********************)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	76
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	77	(Set location of graphics for HTML files)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	78	fun gif_path () = tack_on (normalize_path (!output_dir)) "gif";
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	79
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	80
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	81	(Name of theory currently being read)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	82	val cur_thyname = ref "";
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	83
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	84
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	85	(Name of current logic)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	86	val package = ref "";
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	87
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	88
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	89	(* Return path of directory where to store html / graph data
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	90	corresponding to theory with given path *)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	91	local
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	92	fun make_path q p =
3748 e5d2399a154f Changed html data directory and names of graph files. berghofe parents: 3639 diff changeset	93	let val outp_dir = normalize_path (!output_dir);
e5d2399a154f Changed html data directory and names of graph files. berghofe parents: 3639 diff changeset	94	val base = if q = "" then outp_dir else tack_on outp_dir q;
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	95	val rpath = if p subdir_of (!base_path) then relative_path (!base_path) p
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	96	else relative_path (normalize_path (!home_path)) p;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	97	in tack_on base rpath end
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	98	in
3748 e5d2399a154f Changed html data directory and names of graph files. berghofe parents: 3639 diff changeset	99	val html_path = make_path "";
3639 dc998476ce76 Modified graph data directory. berghofe parents: 3628 diff changeset	100	val graph_path = make_path "graph/data"
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	101	end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	102
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	103
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	104	(Location of theory-list.txt and index.html (set by init_html))
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	105	val index_path = ref "";
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	106
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	107
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	108	(Original path of ROOT.ML)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	109	val original_path = ref "";
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	110
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	111
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	112	(Location of Pure_sub.html and CPure_sub.html)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	113	val pure_subchart = ref (None : string option);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	114
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	115
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	116	(Controls whether HTML files should be generated)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	117	val make_html = ref false;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	118
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	119
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	120	(*HTML file of theory currently being read
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	121	(Initialized by thyfile2html; used by use_thy and store_thm)*)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	122	val cur_htmlfile = ref None : TextIO.outstream option ref;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	123
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	124
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	125	(*Boolean variable which indicates if the title "Theorems proved in foo.ML"
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	126	has already been inserted into the current HTML file*)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	127	val cur_has_title = ref false;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	128
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	129
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	130	(*Make head of HTML dependency charts
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	131	Parameters are:
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	132	file: HTML file
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	133	tname: theory name
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	134	suffix: suffix of complementary chart
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	135	(sup if this head is for a sub-chart, sub if it is for a sup-chart;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	136	empty for Pure and CPure sub-charts)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	137	gif_path: relative path to directory containing GIFs
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	138	index_path: relative path to directory containing main theory chart
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	139	*)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	140	fun mk_charthead file tname title repeats gif_path index_path package =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	141	TextIO.output (file,
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	142	"<HTML><HEAD><TITLE>" ^ title ^ " of " ^ tname ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	143	"</TITLE></HEAD>\n<H2>" ^ title ^ " of theory " ^ tname ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	144	"</H2>\nThe name of every theory is linked to its theory file<BR>\n" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	145	"<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	146	\\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	147	\<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	148	\\" ALT = /\\></A> stands for supertheories (parent theories)\n" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	149	(if not repeats then "" else
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	150	"<BR><TT>...</TT> stands for repeated subtrees") ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	151	"<P>\n<A HREF = \"" ^ tack_on index_path "index.html\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	152	\\">Back</A> to the index of " ^ package ^ "\n<HR>\n<PRE>");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	153
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	154
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	155	(Convert special HTML characters ('&', '>', and '<'))
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	156	fun escape [] = []
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	157	\| escape ("<"::s) = "<" :: escape s
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	158	\| escape (">"::s) = ">" :: escape s
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	159	\| escape ("&"::s) = "&" :: escape s
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	160	\| escape (c::s) = c :: escape s;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	161
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	162
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	163	(Convert .thy file to HTML and make chart of its super-theories)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	164	fun thyfile2html tname thy_path = if not (!make_html) then () else
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	165	let
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	166	(* path of directory, where corresponding HTML file is stored *)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	167	val tpath = html_path thy_path;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	168
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	169	(* gif directory *)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	170	val rel_gif_path = relative_path tpath (gif_path ());
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	171
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	172	val rel_index_path = relative_path tpath (!index_path);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	173
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	174	(Make list of all theories and all theories that own a .thy file)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	175	fun list_theories [] theories thy_files = (theories, thy_files)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	176	\| list_theories ((tname, ThyInfo {thy_time, ...}) :: ts)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	177	theories thy_files =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	178	list_theories ts (tname :: theories)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	179	(if is_some thy_time andalso the thy_time <> "" then
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	180	tname :: thy_files
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	181	else thy_files);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	182
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	183	val (theories, thy_files) =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	184	list_theories (Symtab.dest (!loaded_thys)) [] [];
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	185
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	186	(convert ML file to html )
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	187	fun ml2html name abs_path =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	188	let val is = TextIO.openIn (tack_on abs_path (name ^ ".ML"));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	189	val inp = implode (escape (explode (TextIO.inputAll is)));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	190	val _ = TextIO.closeIn is;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	191	val os = TextIO.openOut (tack_on (html_path abs_path) (name ^ "_ML.html"));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	192	val _ = TextIO.output (os,
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	193	"<HTML><HEAD><TITLE>" ^ name ^ ".ML</TITLE></HEAD>\n\n<BODY>\n" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	194	"<H2>" ^ name ^ ".ML</H2>\n<A HREF = \"" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	195	name ^ ".html\">Back</A> to theory " ^ name ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	196	"\n<HR>\n\n<PRE>\n" ^ inp ^ "</PRE><HR></BODY></HTML>");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	197	val _ = TextIO.closeOut os;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	198	in () end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	199
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	200	(Do the conversion)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	201	fun gettext thy_file =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	202	let
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	203	(Convert special HTML characters ('&', '>', and '<'))
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	204	val file =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	205	let val is = TextIO.openIn thy_file;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	206	val inp = TextIO.inputAll is;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	207	in (TextIO.closeIn is; escape (explode inp)) end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	208
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	209
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	210	(*Isolate first (possibly nested) comment;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	211	skip all leading whitespaces*)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	212	val (comment, file') =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	213	let fun first_comment ("" :: ")" :: cs) co 1 = (co ^ ")", cs)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	214	\| first_comment ("*" :: ")" :: cs) co d =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	215	first_comment cs (co ^ "*)") (d-1)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	216	\| first_comment ("(" :: "*" :: cs) co d =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	217	first_comment cs (co ^ "(*") (d+1)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	218	\| first_comment (" " :: cs) "" 0 = first_comment cs "" 0
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	219	\| first_comment ("\n" :: cs) "" 0 = first_comment cs "" 0
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	220	\| first_comment ("\t" :: cs) "" 0 = first_comment cs "" 0
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	221	\| first_comment cs "" 0 = ("", cs)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	222	\| first_comment (c :: cs) co d =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	223	first_comment cs (co ^ implode [c]) d
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	224	\| first_comment [] co _ =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	225	error ("Unexpected end of file " ^ tname ^ ".thy.");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	226	in first_comment file "" 0 end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	227
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	228	(*Process line defining theory's ancestors;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	229	convert valid theory names to links to their HTML file*)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	230	val (ancestors, body) =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	231	let
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	232	fun make_links l result =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	233	let val (pre, letter) = take_prefix (not o is_letter) l;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	234
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	235	val (id, rest) =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	236	take_prefix (is_quasi_letter orf is_digit) letter;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	237
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	238	val id = implode id;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	239
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	240	(Make a HTML link out of a theory name)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	241	fun make_link t =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	242	let val path = html_path (path_of t);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	243	in "<A HREF = \"" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	244	tack_on (relative_path tpath path) t ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	245	".html\">" ^ t ^ "</A>" end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	246	in if not (id mem theories) then (result, implode l)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	247	else if id mem thy_files then
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	248	make_links rest (result ^ implode pre ^ make_link id)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	249	else make_links rest (result ^ implode pre ^ id)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	250	end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	251
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	252	val (pre, rest) = take_prefix (fn c => c <> "=") file';
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	253
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	254	val (ancestors, body) =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	255	if null rest then
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	256	error ("Missing \"=\" in file " ^ tname ^ ".thy.\n\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	257	\(Make sure that the last line ends with a linebreak.)")
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	258	else
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	259	make_links rest "";
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	260	in (implode pre ^ ancestors, body) end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	261	in "<HTML><HEAD><TITLE>" ^ tname ^ ".thy</TITLE></HEAD>\n\n<BODY>\n" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	262	"<H2>" ^ tname ^ ".thy</H2>\n<A HREF = \"" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	263	tack_on rel_index_path "index.html\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	264	\\">Back</A> to the index of " ^ (!package) ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	265	"\n<HR>\n\n<PRE>\n" ^ comment ^ ancestors ^ body ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	266	"</PRE>\n"
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	267	end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	268
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	269	( Make chart of super-theories )
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	270
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	271	val _ = mkdir tpath;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	272	val sup_out = TextIO.openOut (tack_on tpath (tname ^ "_sup.html"));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	273	val sub_out = TextIO.openOut (tack_on tpath (tname ^ "_sub.html"));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	274
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	275	(Theories that already have been listed in this chart)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	276	val listed = ref [];
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	277
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	278	val wanted_theories =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	279	filter (fn s => s mem thy_files orelse s = "Pure" orelse s = "CPure")
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	280	theories;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	281
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	282	(Make tree of theory dependencies)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	283	fun list_ancestors tname level continued =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	284	let
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	285	fun mk_entry [] = ()
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	286	\| mk_entry (t::ts) =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	287	let
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	288	val is_pure = t = "Pure" orelse t = "CPure";
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	289	val path = if is_pure then (the (!pure_subchart))
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	290	else html_path (path_of t);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	291	val rel_path = relative_path tpath path;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	292	val repeated = t mem (!listed) andalso
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	293	not (null (parents_of_name t));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	294
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	295	fun mk_offset [] cur =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	296	if level < cur then error "Error in mk_offset"
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	297	else implode (replicate (level - cur) " ")
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	298	\| mk_offset (l::ls) cur =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	299	implode (replicate (l - cur) " ") ^ "\| " ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	300	mk_offset ls (l+1);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	301	in TextIO.output (sup_out,
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	302	" " ^ mk_offset continued 0 ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	303	"\\__" ^ (if is_pure then t else
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	304	"<A HREF=\"" ^ tack_on rel_path t ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	305	".html\">" ^ t ^ "</A>") ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	306	(if repeated then "..." else " ") ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	307	"<A HREF = \"" ^ tack_on rel_path t ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	308	"_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	309	tack_on rel_gif_path "red_arrow.gif\" ALT = \\/></A>" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	310	(if is_pure then ""
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	311	else "<A HREF = \"" ^ tack_on rel_path t ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	312	"_sup.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	313	tack_on rel_gif_path "blue_arrow.gif\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	314	\\" ALT = /\\></A>") ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	315	"\n");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	316	if repeated then ()
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	317	else (listed := t :: (!listed);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	318	list_ancestors t (level+1) (if null ts then continued
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	319	else continued @ [level]);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	320	mk_entry ts)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	321	end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	322
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	323	val relatives =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	324	filter (fn s => s mem wanted_theories) (parents_of_name tname);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	325	in mk_entry relatives end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	326	in if is_some (!cur_htmlfile) then
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	327	(TextIO.closeOut (the (!cur_htmlfile));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	328	warning "Last theory's HTML file has not been closed.")
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	329	else ();
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	330	cur_htmlfile := Some (TextIO.openOut (tack_on tpath (tname ^ ".html")));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	331	cur_has_title := false;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	332	if file_exists (tack_on thy_path (tname ^ ".ML"))
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	333	then ml2html tname thy_path else ();
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	334	TextIO.output (the (!cur_htmlfile), gettext (tack_on thy_path tname ^ ".thy"));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	335
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	336	mk_charthead sup_out tname "Ancestors" true rel_gif_path rel_index_path
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	337	(!package);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	338	TextIO.output(sup_out,
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	339	"<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	340	\<A HREF = \"" ^ tname ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	341	"_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	342	tack_on rel_gif_path "red_arrow.gif\" ALT = \\/></A>\n");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	343	list_ancestors tname 0 [];
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	344	TextIO.output (sup_out, "</PRE><HR></BODY></HTML>");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	345	TextIO.closeOut sup_out;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	346
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	347	mk_charthead sub_out tname "Children" false rel_gif_path rel_index_path
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	348	(!package);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	349	TextIO.output(sub_out,
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	350	"<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	351	\<A HREF = \"" ^ tname ^ "_sup.html\"><IMG SRC = \"" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	352	tack_on rel_gif_path "blue_arrow.gif\" BORDER=0 ALT = \\/></A>\n");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	353	TextIO.closeOut sub_out
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	354	end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	355
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	356
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	357	(*Makes HTML title for list of theorems; as this list may be empty and we
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	358	don't want a title in that case, mk_theorems_title is only invoked when
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	359	something is added to the list*)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	360	fun mk_theorems_title out =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	361	if not (!cur_has_title) then
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	362	(cur_has_title := true;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	363	TextIO.output (out, "<HR><H2>Theorems proved in <A HREF = \"" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	364	(!cur_thyname) ^ "_ML.html\">" ^ (!cur_thyname) ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	365	".ML</A>:</H2>\n"))
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	366	else ();
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	367
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	368
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	369	exception MK_HTML;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	370
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	371	(*Add theory to file listing all loaded theories (for index.html)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	372	and to the sub-charts of its parents*)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	373	fun mk_html tname abs_path old_parents = if not (!make_html) then () else
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	374	( let val new_parents = parents_of_name tname \\ old_parents;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	375
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	376	fun robust_seq (proc: 'a -> unit) : 'a list -> unit =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	377	let fun seqf [] = ()
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	378	\| seqf (x :: xs) = (proc x handle _ => (); seqf xs)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	379	in seqf end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	380
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	381	(Add child to parents' sub-theory charts)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	382	fun add_to_parents t =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	383	let val path = if t = "Pure" orelse t = "CPure" then
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	384	(the (!pure_subchart))
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	385	else html_path (path_of t);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	386
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	387	val rel_gif_path = relative_path path (gif_path ());
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	388	val rel_path = relative_path path (html_path abs_path);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	389	val tpath = tack_on rel_path tname;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	390
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	391	val fname = tack_on path (t ^ "_sub.html");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	392	val out = if file_exists fname then
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	393	TextIO.openAppend fname handle e =>
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	394	(warning ("Unable to write to file " ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	395	fname); raise e)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	396	else raise MK_HTML;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	397	in TextIO.output (out,
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	398	" \|\n \\__<A HREF=\"" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	399	tack_on rel_path tname ^ ".html\">" ^ tname ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	400	"</A> <A HREF = \"" ^ tpath ^ "_sub.html\">\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	401	\<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	402	tack_on rel_gif_path "red_arrow.gif\" ALT = \\/></A>\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	403	\<A HREF = \"" ^ tpath ^ "_sup.html\">\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	404	\<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	405	tack_on rel_gif_path "blue_arrow.gif\" ALT = /\\></A>\n");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	406	TextIO.closeOut out
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	407	end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	408
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	409	val theory_list =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	410	TextIO.openAppend (tack_on (!index_path) "theory_list.txt")
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	411	handle _ => (make_html := false;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	412	warning ("Cannot write to " ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	413	(!index_path) ^ " while making HTML files.\n\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	414	\HTML generation has been switched off.\n\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	415	\Call init_html() from within a \
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	416	\writeable directory to reactivate it.");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	417	raise MK_HTML)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	418	in TextIO.output (theory_list, tname ^ " " ^ abs_path ^ "\n");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	419	TextIO.closeOut theory_list;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	420	robust_seq add_to_parents new_parents
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	421	end
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	422	) handle MK_HTML => ();
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	423
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	424
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	425	(* Misc HTML functions *)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	426
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	427	(Init HTML generator by setting paths and creating new files)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	428	fun init_html () =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	429	let val cwd = OS.FileSys.getDir();
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	430	val _ = mkdir (html_path cwd);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	431
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	432	val theory_list = TextIO.closeOut (TextIO.openOut (tack_on (html_path cwd) "theory_list.txt"));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	433
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	434	val rel_gif_path = relative_path (html_path cwd) (gif_path ());
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	435
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	436	(Make new HTML files for Pure and CPure)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	437	fun init_pure_html () =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	438	let val pure_out = TextIO.openOut (tack_on (html_path cwd) "Pure_sub.html");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	439	val cpure_out = TextIO.openOut (tack_on (html_path cwd) "CPure_sub.html");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	440	in mk_charthead pure_out "Pure" "Children" false rel_gif_path ""
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	441	(!package);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	442	mk_charthead cpure_out "CPure" "Children" false rel_gif_path ""
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	443	(!package);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	444	TextIO.output (pure_out, "Pure\n");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	445	TextIO.output (cpure_out, "CPure\n");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	446	TextIO.closeOut pure_out;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	447	TextIO.closeOut cpure_out;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	448	pure_subchart := Some (html_path cwd)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	449	end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	450
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	451	in make_html := true;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	452	(*Make sure that base_path contains the physical path and no
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	453	symbolic links*)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	454	base_path := normalize_path (!base_path);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	455	original_path := cwd;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	456	index_path := html_path cwd;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	457	package :=
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	458	(if cwd subdir_of (!base_path) then
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	459	relative_path (!base_path) cwd
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	460	else base_name cwd);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	461
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	462	(*Copy README files to html directory
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	463	FIXME: let usedir do this job*)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	464	copy_file (tack_on cwd "README.html") (tack_on (!index_path) "README.html");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	465	copy_file (tack_on cwd "README") (tack_on (!index_path) "README");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	466
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	467	if cwd subdir_of (!base_path) then ()
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	468	else warning "The current working directory seems to be no \
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	469	\subdirectory of\nIsabelle's main directory. \
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	470	\Please ensure that base_path's value is correct.\n";
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	471
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	472	writeln ("Setting path for index.html to " ^ quote (!index_path) ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	473	"\nGIF path has been set to " ^ quote (gif_path ()));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	474
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	475	if is_none (!pure_subchart) then init_pure_html()
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	476	else ()
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	477	end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	478
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	479
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	480	(Generate index.html)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	481	fun finish_html () = if not (!make_html) then () else
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	482	let val tlist_path = tack_on (!index_path) "theory_list.txt";
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	483	val theory_list = TextIO.openIn tlist_path;
3834 278f0a1e5986 BAD_space_explode; wenzelm parents: 3748 diff changeset	484	val theories = BAD_space_explode "\n" (TextIO.inputAll theory_list);
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	485	val dummy = (TextIO.closeIn theory_list; OS.FileSys.remove tlist_path);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	486
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	487	val rel_gif_path = relative_path (!index_path) (gif_path ());
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	488
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	489	(Make entry for main chart of all theories.)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	490	fun main_entry t =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	491	let
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	492	val (name, path) = take_prefix (not_equal " ") (explode t);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	493
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	494	val tname = implode name
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	495	val tpath = tack_on (relative_path (!index_path) (html_path (implode (tl path))))
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	496	tname;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	497	in "<A HREF = \"" ^ tpath ^ "_sub.html\"><IMG SRC = \"" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	498	tack_on rel_gif_path "red_arrow.gif\" BORDER=0 ALT = \\/></A>" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	499	"<A HREF = \"" ^ tpath ^ "_sup.html\"><IMG SRC = \"" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	500	tack_on rel_gif_path "blue_arrow.gif\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	501	\\" BORDER=0 ALT = /\\></A> <A HREF = \"" ^ tpath ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	502	".html\">" ^ tname ^ "</A><BR>\n"
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	503	end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	504
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	505	val out = TextIO.openOut (tack_on (!index_path) "index.html");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	506
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	507	(*Find out in which subdirectory of Isabelle's main directory the
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	508	index.html is placed; if original_path is no subdirectory of base_path
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	509	then take the last directory of index_path*)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	510	val inside_isabelle = (!original_path) subdir_of (!base_path);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	511	val subdir =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	512	if inside_isabelle then relative_path (html_path (!base_path)) (!index_path)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	513	else base_name (!index_path);
3834 278f0a1e5986 BAD_space_explode; wenzelm parents: 3748 diff changeset	514	val subdirs = BAD_space_explode "/" subdir;
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	515
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	516	(*Look for index.html in superdirectories; stop when Isabelle's
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	517	main directory is reached*)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	518	fun find_super_index [] n = ("", n)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	519	\| find_super_index (p::ps) n =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	520	let val index_path = "/" ^ space_implode "/" (rev ps);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	521	in if file_exists (index_path ^ "/index.html") then (index_path, n)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	522	else if length subdirs - n > 0 then find_super_index ps (n+1)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	523	else ("", n)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	524	end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	525	val (super_index, level_diff) =
3834 278f0a1e5986 BAD_space_explode; wenzelm parents: 3748 diff changeset	526	find_super_index (rev (BAD_space_explode "/" (!index_path))) 1;
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	527	val level = length subdirs - level_diff;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	528
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	529	(Add link to current directory to 'super' index.html)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	530	fun link_directory () =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	531	let val old_index = TextIO.openIn (super_index ^ "/index.html");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	532	val content = rev (explode (TextIO.inputAll old_index));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	533	val dummy = TextIO.closeIn old_index;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	534
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	535	val out = TextIO.openAppend (super_index ^ "/index.html");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	536	val rel_path = space_implode "/" (drop (level, subdirs));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	537	in
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	538	TextIO.output (out,
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	539	(if nth_elem (3, content) <> "!" then ""
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	540	else "\n<HR><H3>Subdirectories:</H3>\n") ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	541	"<H3><A HREF = \"" ^ rel_path ^ "/index.html\">" ^ rel_path ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	542	"</A></H3>\n");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	543	TextIO.closeOut out
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	544	end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	545
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	546	(*If original_path is no subdirectory of base_path then the title should
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	547	not contain the string "Isabelle/"*)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	548	val title = (if inside_isabelle then "Isabelle/" else "") ^ subdir;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	549	val rel_graph_path = tack_on (relative_path (!index_path) (graph_path (!original_path)))
3748 e5d2399a154f Changed html data directory and names of graph files. berghofe parents: 3639 diff changeset	550	"small.html"
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	551	in TextIO.output (out,
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	552	"<HTML><HEAD><TITLE>" ^ title ^ "</TITLE></HEAD>\n\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	553	\<BODY><H2>" ^ title ^ "</H2>\n\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	554	\The name of every theory is linked to its theory file<BR>\n\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	555	\<IMG SRC = \"" ^ tack_on rel_gif_path "red_arrow.gif\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	556	\\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	557	\<IMG SRC = \"" ^ tack_on rel_gif_path "blue_arrow.gif\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	558	\\" ALT = /\\></A> stands for supertheories (parent theories)<P>\n\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	559	\View <A HREF=\"" ^ rel_graph_path ^ "\">graph</A> of theories<P>\n" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	560	(if super_index = "" then "" else
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	561	("<A HREF = \"" ^ relative_path (!index_path) super_index ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	562	"/index.html\">Back</A> to the index of " ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	563	(if not inside_isabelle then
3834 278f0a1e5986 BAD_space_explode; wenzelm parents: 3748 diff changeset	564	hd (tl (rev (BAD_space_explode "/" (!index_path))))
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	565	else if level = 0 then "Isabelle logics"
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	566	else space_implode "/" (take (level, subdirs))))) ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	567	"\n" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	568	(if file_exists (tack_on (!index_path) "README.html") then
3868 86981c4bffdb tuned; wenzelm parents: 3834 diff changeset	569	"<BR>View the <A HREF = \"README.html\">README</A> file.\n"
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	570	else if file_exists (tack_on (!index_path) "README") then
3868 86981c4bffdb tuned; wenzelm parents: 3834 diff changeset	571	"<BR>View the <A HREF = \"README\">README</A> file.\n"
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	572	else "") ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	573	"<HR>" ^ implode (map main_entry theories) ^ "<!-->");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	574	TextIO.closeOut out;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	575	if super_index = "" orelse (inside_isabelle andalso level = 0) then ()
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	576	else link_directory ()
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	577	end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	578
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	579
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	580	(Append section heading to HTML file)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	581	fun section s =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	582	case !cur_htmlfile of
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	583	Some out => (mk_theorems_title out;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	584	TextIO.output (out, "<H3>" ^ s ^ "</H3>\n"))
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	585	\| None => ();
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	586
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	587
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	588	(Add theorem to HTML file)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	589	fun thm_to_html thm name =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	590	case !cur_htmlfile of
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	591	Some out =>
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	592	(mk_theorems_title out;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	593	TextIO.output (out, "<DD><EM>" ^ name ^ "</EM>\n<PRE>" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	594	(implode o escape)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	595	(explode
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	596	(string_of_thm (#1 (freeze_thaw thm)))) ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	597	"</PRE><P>\n")
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	598	)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	599	\| None => ();
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	600
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	601
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	602	(Close HTML file)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	603	fun close_html () =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	604	case !cur_htmlfile of
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	605	Some out => (TextIO.output (out, "<HR></BODY></HTML>\n");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	606	TextIO.closeOut out;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	607	cur_htmlfile := None)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	608	\| None => () ;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	609
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	610
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	611	(****************** Graph generation functions **********************)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	612
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	613
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	614	(flag that indicates whether graph files should be generated)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	615	val make_graph = ref false;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	616
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	617
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	618	(file to use as basis for new graph files)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	619	val graph_base_file = ref "";
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	620
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	621
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	622	(directory containing basic theories (gets label "base"))
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	623	val graph_root_dir = ref "";
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	624
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	625
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	626	(name of current graph file)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	627	val graph_file = ref "";
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	628
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	629
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	630	(*name of large graph file which also contains
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	631	theories defined in subdirectories *)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	632	val large_graph_file = ref "";
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	633
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	634
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	635	(* initialize graph data generator *)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	636	fun init_graph usedir_arg =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	637	let
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	638	(create default graph containing only Pure, CPure and ProtoPure)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	639	fun default_graph outfile =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	640	let val os = TextIO.openOut outfile;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	641	in (TextIO.output(os,"\"ProtoPure\" \"ProtoPure\" \"Pure\" \"\" ;\n\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	642	\\"CPure\" \"CPure\" \"Pure\" \"\" > \"ProtoPure\" ;\n\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	643	\\"Pure\" \"Pure\" \"Pure\" \"\" > \"ProtoPure\" ;\n");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	644	TextIO.closeOut os)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	645	end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	646
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	647	(copy graph file, adjust relative paths for theory files)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	648	fun copy_graph infile outfile unfold =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	649	let val is = TextIO.openIn infile;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	650	val (inp_dir, _) = split_filename infile;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	651	val (outp_dir, _) = split_filename outfile;
3834 278f0a1e5986 BAD_space_explode; wenzelm parents: 3748 diff changeset	652	val entries = map (BAD_space_explode " ")
278f0a1e5986 BAD_space_explode; wenzelm parents: 3748 diff changeset	653	(BAD_space_explode "\n" (TextIO.inputAll is));
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	654
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	655	fun thyfile f = if f = "\"\"" then f else
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	656	let val (dir, name) =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	657	split_filename (implode (rev (tl (rev (tl (explode f))))));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	658	val abs_path = normalize_path (tack_on inp_dir dir);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	659	val rel_path = tack_on (relative_path outp_dir abs_path) name
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	660	in quote rel_path end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	661
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	662	fun process_entry (a::b::c::d::e::r) =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	663	if d = "+" then
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	664	a::b::c::((if unfold then "+ " else "") ^ (thyfile e))::r
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	665	else
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	666	a::b::c::(thyfile d)::e::r;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	667
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	668	val _ = TextIO.closeIn is;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	669	val os = TextIO.openOut outfile;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	670	val _ = TextIO.output(os, (cat_lines
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	671	(map ((space_implode " ") o process_entry) entries)) ^ "\n");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	672	val _ = TextIO.closeOut os;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	673	in () end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	674
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	675	(create html page which contains graph browser applet)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	676	fun mk_applet_page abs_path large other_graph =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	677	let
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	678	val dir_name =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	679	(if (!original_path) subdir_of (!base_path) then "Isabelle/" else "") ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	680	(relative_path (normalize_path (tack_on (!graph_root_dir) "..")) (pwd ()));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	681	val rel_codebase =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	682	relative_path abs_path (tack_on (normalize_path (!output_dir)) "graph");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	683	val rel_index_path = tack_on (relative_path
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	684	abs_path (tack_on (normalize_path (!output_dir)) "graph")) "index.html";
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	685	val outfile =
3748 e5d2399a154f Changed html data directory and names of graph files. berghofe parents: 3639 diff changeset	686	tack_on abs_path ((if large then "large" else "small") ^ ".html");
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	687	val os = TextIO.openOut outfile;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	688	val _ = TextIO.output(os,
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	689	"<HTML><HEAD><TITLE>" ^ dir_name ^ "</TITLE></HEAD>\n\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	690	\<BODY><H2>" ^ dir_name ^ "</H2>\n" ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	691	(if other_graph then
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	692	(if large then
3748 e5d2399a154f Changed html data directory and names of graph files. berghofe parents: 3639 diff changeset	693	"View <A HREF=\"small.html\">small graph</A> without \
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	694	\subdirectories<P>\n"
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	695	else
3748 e5d2399a154f Changed html data directory and names of graph files. berghofe parents: 3639 diff changeset	696	"View <A HREF=\"large.html\">large graph</A> including \
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	697	\all subdirectories<P>\n")
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	698	else "") ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	699	"<A HREF=\"" ^ rel_index_path ^ "\">Back</A> to index\n<HR>\n\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	700	\<APPLET CODE=\"GraphBrowser/GraphBrowser.class\" \
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	701	\CODEBASE=\"" ^ rel_codebase ^ "\" WIDTH=550 HEIGHT=450>\n\
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	702	\<PARAM NAME=\"graphfile\" VALUE=\"" ^
3748 e5d2399a154f Changed html data directory and names of graph files. berghofe parents: 3639 diff changeset	703	(if large then "large.graph" else "small.graph") ^ "\">\n\
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	704	\</APPLET>\n<HR>\n</BODY></HTML>")
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	705	val _ = TextIO.closeOut os
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	706	in () end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	707
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	708	val gpath = graph_path (pwd ());
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	709
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	710	in
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	711	(make_graph := true;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	712	base_path := normalize_path (!base_path);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	713	mkdir gpath;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	714	original_path := pwd ();
3748 e5d2399a154f Changed html data directory and names of graph files. berghofe parents: 3639 diff changeset	715	graph_file := tack_on gpath "small.graph";
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	716	graph_root_dir := (if usedir_arg = "." then pwd ()
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	717	else normalize_path (tack_on (pwd ()) ".."));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	718	(if (!graph_base_file) = "" then
3748 e5d2399a154f Changed html data directory and names of graph files. berghofe parents: 3639 diff changeset	719	(large_graph_file := tack_on gpath "large.graph";
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	720	default_graph (!graph_file);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	721	default_graph (!large_graph_file);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	722	mk_applet_page gpath false true;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	723	mk_applet_page gpath true true)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	724	else
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	725	(if (fst (split_filename (!graph_file))) subdir_of
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	726	(fst (split_filename (!graph_base_file)))
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	727	then
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	728	(copy_graph (!graph_base_file) (!graph_file) true;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	729	mk_applet_page gpath false false)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	730	else
3748 e5d2399a154f Changed html data directory and names of graph files. berghofe parents: 3639 diff changeset	731	(large_graph_file := tack_on gpath "large.graph";
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	732	mk_applet_page gpath false true;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	733	mk_applet_page gpath true true;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	734	copy_graph (!graph_base_file) (!graph_file) false;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	735	copy_graph (!graph_base_file) (!large_graph_file) false)));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	736	graph_base_file := (!graph_file))
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	737	end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	738
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	739
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	740	(add theory to graph definition file)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	741	fun mk_graph tname abs_path = if not (!make_graph) then () else
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	742	let val parents =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	743	map (fn (t, _) => tack_on (path_of t) t)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	744	(filter (fn (_, ThyInfo {children,...}) => tname mem children)
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	745	(Symtab.dest(!loaded_thys)));
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	746
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	747	val dir_name = relative_path
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	748	(normalize_path (tack_on (!graph_root_dir) "..")) abs_path;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	749
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	750	val dir_entry = "\"" ^ dir_name ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	751	(if (tack_on abs_path "") = (tack_on (!graph_root_dir) "")
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	752	then "/base\" + " else "\" ");
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	753
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	754	val thy_file = (tack_on (html_path abs_path) tname) ^ ".html";
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	755
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	756	val thy_ID = quote (tack_on abs_path tname);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	757
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	758	val entry_str_1 = (quote tname) ^ " " ^ thy_ID ^ " " ^ dir_entry ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	759	(quote (relative_path (fst (split_filename (!graph_file))) thy_file)) ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	760	" > " ^ (space_implode " " (map quote parents)) ^ " ;\n" ;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	761
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	762	val entry_str_2 = (quote tname) ^ " " ^ thy_ID ^ " " ^ dir_entry ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	763	(quote (relative_path (fst (split_filename (!large_graph_file))) thy_file)) ^
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	764	" > " ^ (space_implode " " (map quote parents)) ^ " ;\n" ;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	765
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	766	fun exists_entry id infile =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	767	let val is = TextIO.openIn(infile);
3834 278f0a1e5986 BAD_space_explode; wenzelm parents: 3748 diff changeset	768	val IDs = map (hd o tl o (BAD_space_explode " "))
278f0a1e5986 BAD_space_explode; wenzelm parents: 3748 diff changeset	769	(BAD_space_explode "\n" (TextIO.inputAll is));
3603 5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	770	val _ = TextIO.closeIn is
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	771	in id mem IDs end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	772
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	773	fun mk_entry outfile entry_str =
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	774	if exists_entry thy_ID outfile then ()
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	775	else
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	776	let val os = TextIO.openAppend outfile;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	777	val _ = TextIO.output (os, entry_str);
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	778	val _ = TextIO.closeOut os;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	779	in () end
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	780
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	781	in (mk_entry (!graph_file) entry_str_1;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	782	mk_entry (!large_graph_file) entry_str_2) handle _ =>
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	783	(make_graph:=false;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	784	warning ("Unable to write to graph file " ^ (!graph_file)))
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	785	end;
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	786
5eef2ff0eb72 This file now contains all functions for generating html berghofe parents: diff changeset	787	end;

author	wenzelm
	Mon, 20 Oct 1997 15:20:20 +0200
changeset 3956	d59fe4579004
parent 3870	6913700d7c79
child 3976	1030dd79720b
permissions	-rw-r--r--