author  nipkow 
Thu, 14 Nov 1996 16:01:36 +0100  
changeset 2188  6c217c071b97 
parent 2030  474b3f208789 
child 2244  dacee519738a 
permissions  rwrr 
391  1 
(* Title: Pure/Thy/thy_read.ML 
2 
ID: $Id$ 

559  3 
Author: Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and 
4 
Tobias Nipkow and L C Paulson 

5 
Copyright 1994 TU Muenchen 

391  6 

1242  7 
Functions for reading theory files, and storing and retrieving theories, 
8 
theorems and the global simplifier set. 

391  9 
*) 
10 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

11 
(*Types for theory storage*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

12 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

13 
(*Functions to handle arbitrary data added by the user; type "exn" is used 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

14 
to store data*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

15 
datatype thy_methods = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

16 
ThyMethods of {merge: exn list > exn, put: exn > unit, get: unit > exn}; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

17 

1291  18 
datatype thy_info = 
19 
ThyInfo of {path: string, 

20 
children: string list, parents: string list, 

21 
thy_time: string option, ml_time: string option, 

22 
theory: theory option, thms: thm Symtab.table, 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

23 
methods: thy_methods Symtab.table, 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

24 
data: exn Symtab.table * exn Symtab.table}; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

25 
(*thy_time, ml_time = None theory file has not been read yet 
1157  26 
= Some "" theory was read but has either been marked 
27 
as outdated or there is no such file for 

28 
this theory (see e.g. 'virtual' theories 

29 
like Pure or theories without a ML file) 

30 
theory = None theory has not been read yet 

1291  31 

32 
parents: While 'children' contains all theories the theory depends 

33 
on (i.e. also ones quoted in the .thy file), 

34 
'parents' only contains the theories which were used to form 

35 
the base of this theory. 

36 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

37 
methods: three methods for each user defined data; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

38 
merge: merges data of ancestor theories 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

39 
put: retrieves data from loaded_thys and stores it somewhere 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

40 
get: retrieves data from somewhere and stores it 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

41 
in loaded_thys 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

42 
Warning: If these functions access reference variables inside 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

43 
READTHY, they have to be redefined each time 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

44 
init_thy_reader is invoked 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

45 
data: user defined data; exn is used to allow arbitrary types; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

46 
first element of pairs contains result that get returned after 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

47 
thy file was read, second element after ML file was read 
1157  48 
*) 
391  49 

412  50 
signature READTHY = 
391  51 
sig 
52 
datatype basetype = Thy of string 

53 
 File of string 

54 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

55 
val loaded_thys : thy_info Symtab.table ref 
391  56 
val loadpath : string list ref 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

57 
val thy_reader_files: string list ref 
391  58 
val delete_tmpfiles: bool ref 
59 

60 
val use_thy : string > unit 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

61 
val time_use_thy : string > unit 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

62 
val use_dir : string > unit 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

63 
val exit_use_dir : string > unit 
391  64 
val update : unit > unit 
65 
val unlink_thy : string > unit 

586
201e115d8031
renamed base_on into mk_base and moved it to the beginning of the generated
clasohm
parents:
559
diff
changeset

66 
val mk_base : basetype list > string > bool > theory 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

67 
val store_theory : theory * string > unit 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

68 

1403
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

69 
val theory_of : string > theory 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

70 
val theory_of_sign : Sign.sg > theory 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

71 
val theory_of_thm : thm > theory 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

72 
val children_of : string > string list 
1403
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

73 
val parents_of_name: string > string list 
1664  74 
val thyname_of_sign: Sign.sg > string 
1291  75 

1603
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

76 
val store_thm : string * thm > thm 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

77 
val bind_thm : string * thm > unit 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

78 
val qed : string > unit 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

79 
val qed_thm : thm ref 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

80 
val qed_goal : string > theory > string 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

81 
> (thm list > tactic list) > unit 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

82 
val qed_goalw : string > theory > thm list > string 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

83 
> (thm list > tactic list) > unit 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

84 
val get_thm : theory > string > thm 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

85 
val thms_of : theory > (string * thm) list 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

86 
val delete_thms : string > unit 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

87 

1658
0eb69773354f
add_thydata and get_thydata now take a string as their first argument
clasohm
parents:
1656
diff
changeset

88 
val add_thydata : string > string * thy_methods > unit 
0eb69773354f
add_thydata and get_thydata now take a string as their first argument
clasohm
parents:
1656
diff
changeset

89 
val get_thydata : string > string > exn option 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

90 
val add_thy_reader_file: string > unit 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

91 
val set_thy_reader_file: string > unit 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

92 
val read_thy_reader_files: unit > unit 
1603
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

93 
val set_current_thy: string > unit 
1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset

94 

1603
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

95 
val print_theory : theory > unit 
1291  96 

1603
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

97 
val base_path : string ref 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

98 
val gif_path : string ref 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

99 
val index_path : string ref 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

100 
val pure_subchart : string option ref 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

101 
val make_html : bool ref 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

102 
val init_html : unit > unit 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

103 
val finish_html : unit > unit 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

104 
val section : string > unit 
391  105 
end; 
106 

107 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

108 
functor ReadthyFun(structure ThySyn: THY_SYN and ThmDB: THMDB): READTHY = 
391  109 
struct 
1242  110 

111 
open ThmDB Simplifier; 

391  112 

113 
datatype basetype = Thy of string 

114 
 File of string; 

115 

1291  116 
val loaded_thys = 
117 
ref (Symtab.make [("ProtoPure", 

118 
ThyInfo {path = "", 

119 
children = ["Pure", "CPure"], parents = [], 

120 
thy_time = Some "", ml_time = Some "", 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

121 
theory = Some proto_pure_thy, 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

122 
thms = Symtab.null, methods = Symtab.null, 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

123 
data = (Symtab.null, Symtab.null)}), 
1291  124 
("Pure", 
125 
ThyInfo {path = "", children = [], 

126 
parents = ["ProtoPure"], 

127 
thy_time = Some "", ml_time = Some "", 

128 
theory = Some pure_thy, thms = Symtab.null, 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

129 
methods = Symtab.null, 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

130 
data = (Symtab.null, Symtab.null)}), 
1291  131 
("CPure", 
132 
ThyInfo {path = "", 

133 
children = [], parents = ["ProtoPure"], 

134 
thy_time = Some "", ml_time = Some "", 

135 
theory = Some cpure_thy, 

136 
thms = Symtab.null, 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

137 
methods = Symtab.null, 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

138 
data = (Symtab.null, Symtab.null)}) 
1291  139 
]); 
391  140 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

141 
(*Default search path for theory files*) 
1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

142 
val loadpath = ref ["."]; 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

143 

35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

144 
(*Directory given as parameter to use_thy. This is temporarily added to 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

145 
loadpath while the theory's ancestors are loaded.*) 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

146 
val tmp_loadpath = ref [] : string list ref; 
1291  147 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

148 
(*ML files to be read by init_thy_reader; they normally contain redefinitions 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

149 
of functions accessing reference variables inside READTHY*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

150 
val thy_reader_files = ref [] : string list ref; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

151 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

152 
(*Remove temporary files after use*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

153 
val delete_tmpfiles = ref true; 
1291  154 

391  155 

1291  156 
(*Set location of graphics for HTML files 
157 
(When this is executed for the first time we are in $ISABELLE/Pure/Thy. 

158 
This path is converted to $ISABELLE/Tools by removing the last two 

159 
directories and appending "Tools". All subsequently made ReadThy 

160 
structures inherit this value.) 

161 
*) 

162 
val gif_path = ref (tack_on ("/" ^ 

163 
space_implode "/" (rev (tl (tl (rev (space_explode "/" (pwd ()))))))) 

164 
"Tools"); 

165 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

166 
(*Path of Isabelle's main directory*) 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

167 
val base_path = ref ( 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

168 
"/" ^ space_implode "/" (rev (tl (tl (rev (space_explode "/" (pwd ()))))))); 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

169 

b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

170 

b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

171 
(** HTML variables **) 
1291  172 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

173 
(*Location of .theorylist.txt and index.html (set by init_html)*) 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

174 
val index_path = ref ""; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

175 

b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

176 
(*Location of .Pure_sub.html and .CPure_sub.html*) 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

177 
val pure_subchart = ref (None : string option); 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

178 

b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

179 
(*Controls whether HTML files should be generated*) 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

180 
val make_html = ref false; 
1291  181 

182 
(*HTML file of theory currently being read 

183 
(Initialized by thyfile2html; used by use_thy and store_thm)*) 

184 
val cur_htmlfile = ref None : outstream option ref; 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

185 

b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

186 
(*Boolean variable which indicates if the title "Theorems proved in foo.ML" 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

187 
has already been inserted into the current HTML file*) 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

188 
val cur_has_title = ref false; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

189 

b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

190 
(*Name of theory currently being read*) 
1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset

191 
val cur_thyname = ref ""; 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

192 

b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

193 

391  194 

195 
(*Make name of the output ML file for a theory *) 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

196 
fun out_name tname = "." ^ tname ^ ".thy.ML"; 
391  197 

198 
(*Read a file specified by thy_file containing theory thy *) 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

199 
fun read_thy tname thy_file = 
559  200 
let 
391  201 
val instream = open_in thy_file; 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

202 
val outstream = open_out (out_name tname); 
559  203 
in 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

204 
output (outstream, ThySyn.parse tname (input (instream, 999999))); 
391  205 
close_out outstream; 
206 
close_in instream 

207 
end; 

208 

1480  209 
fun file_exists file = (file_info file <> ""); 
391  210 

1589
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

211 
(*Get last directory in path (e.g. /usr/proj/isabelle > isabelle) *) 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

212 
fun last_path s = case space_explode "/" s of 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

213 
[] => "" 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

214 
 ds => last_elem ds; 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

215 

391  216 
(*Get thy_info for a loaded theory *) 
559  217 
fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname); 
391  218 

971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset

219 
(*Check if a theory was completly loaded *) 
391  220 
fun already_loaded thy = 
221 
let val t = get_thyinfo thy 

222 
in if is_none t then false 

971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset

223 
else let val ThyInfo {thy_time, ml_time, ...} = the t 
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset

224 
in is_some thy_time andalso is_some ml_time end 
391  225 
end; 
226 

227 
(*Check if a theory file has changed since its last use. 

228 
Return a pair of boolean values for .thy and for .ML *) 

559  229 
fun thy_unchanged thy thy_file ml_file = 
1098
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

230 
case get_thyinfo thy of 
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

231 
Some (ThyInfo {thy_time, ml_time, ...}) => 
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

232 
let val tn = is_none thy_time; 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

233 
val mn = is_none ml_time 
391  234 
in if not tn andalso not mn then 
1098
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

235 
((file_info thy_file = the thy_time), 
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

236 
(file_info ml_file = the ml_time)) 
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

237 
else if not tn andalso mn then 
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

238 
(file_info thy_file = the thy_time, false) 
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

239 
else 
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

240 
(false, false) 
391  241 
end 
1098
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

242 
 None => (false, false) 
391  243 

1291  244 
(*Get all direct descendants of a theory*) 
245 
fun children_of t = 

246 
case get_thyinfo t of Some (ThyInfo {children, ...}) => children 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

247 
 None => []; 
1291  248 

1242  249 
(*Get all direct ancestors of a theory*) 
1403
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

250 
fun parents_of_name t = 
1291  251 
case get_thyinfo t of Some (ThyInfo {parents, ...}) => parents 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

252 
 None => []; 
1242  253 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

254 
(*Get all descendants of a theory list *) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

255 
fun get_descendants [] = [] 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

256 
 get_descendants (t :: ts) = 
1291  257 
let val children = children_of t 
258 
in children union (get_descendants (children union ts)) end; 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

259 

1242  260 
(*Get theory object for a loaded theory *) 
1291  261 
fun theory_of name = 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

262 
case get_thyinfo name of Some (ThyInfo {theory = Some t, ...}) => t 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

263 
 _ => error ("Theory " ^ name ^ 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

264 
" not stored by loader"); 
1242  265 

1291  266 
(*Get path where theory's files are located*) 
267 
fun path_of tname = 

268 
let val ThyInfo {path, ...} = the (get_thyinfo tname) 

269 
in path end; 

270 

391  271 
(*Find a file using a list of paths if no absolute or relative path is 
272 
specified.*) 

273 
fun find_file "" name = 

1291  274 
let fun find_it (cur :: paths) = 
275 
if file_exists (tack_on cur name) then 

276 
(if cur = "." then name else tack_on cur name) 

559  277 
else 
1291  278 
find_it paths 
391  279 
 find_it [] = "" 
1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

280 
in find_it (!tmp_loadpath @ !loadpath) end 
391  281 
 find_file path name = 
282 
if file_exists (tack_on path name) then tack_on path name 

283 
else ""; 

284 

285 
(*Get absolute pathnames for a new or already loaded theory *) 

286 
fun get_filenames path name = 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

287 
let fun new_filename () = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

288 
let val found = find_file path (name ^ ".thy"); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

289 
val absolute_path = absolute_path (pwd ()); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

290 
val thy_file = absolute_path found; 
391  291 
val (thy_path, _) = split_filename thy_file; 
292 
val found = find_file path (name ^ ".ML"); 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

293 
val ml_file = if thy_file = "" then absolute_path found 
391  294 
else if file_exists (tack_on thy_path (name ^ ".ML")) 
295 
then tack_on thy_path (name ^ ".ML") 

296 
else ""; 

1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

297 
val searched_dirs = if path = "" then (!tmp_loadpath @ !loadpath) 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

298 
else [path] 
391  299 
in if thy_file = "" andalso ml_file = "" then 
300 
error ("Could not find file \"" ^ name ^ ".thy\" or \"" 

301 
^ name ^ ".ML\" for theory \"" ^ name ^ "\"\n" 

302 
^ "in the following directories: \"" ^ 

303 
(space_implode "\", \"" searched_dirs) ^ "\"") 

304 
else (); 

559  305 
(thy_file, ml_file) 
391  306 
end; 
307 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

308 
val tinfo = get_thyinfo name; 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

309 
in if is_some tinfo andalso path = "" then 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

310 
let val ThyInfo {path = abs_path, ...} = the tinfo; 
391  311 
val (thy_file, ml_file) = if abs_path = "" then new_filename () 
312 
else (find_file abs_path (name ^ ".thy"), 

313 
find_file abs_path (name ^ ".ML")) 

314 
in if thy_file = "" andalso ml_file = "" then 

1580
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1554
diff
changeset

315 
(warning ("File \"" ^ (tack_on path name) 
391  316 
^ ".thy\"\ncontaining theory \"" ^ name 
317 
^ "\" no longer exists."); 

318 
new_filename () 

319 
) 

320 
else (thy_file, ml_file) 

321 
end 

322 
else new_filename () 

323 
end; 

324 

325 
(*Remove theory from all child lists in loaded_thys *) 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

326 
fun unlink_thy tname = 
1291  327 
let fun remove (ThyInfo {path, children, parents, thy_time, ml_time, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

328 
theory, thms, methods, data}) = 
1291  329 
ThyInfo {path = path, children = children \ tname, parents = parents, 
1242  330 
thy_time = thy_time, ml_time = ml_time, theory = theory, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

331 
thms = thms, methods = methods, data = data} 
559  332 
in loaded_thys := Symtab.map remove (!loaded_thys) end; 
391  333 

334 
(*Remove a theory from loaded_thys *) 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

335 
fun remove_thy tname = 
559  336 
loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname) 
337 
(Symtab.dest (!loaded_thys))); 

391  338 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

339 
(*Change thy_time and ml_time for an existent item *) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

340 
fun set_info tname thy_time ml_time = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

341 
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of 
1291  342 
Some (ThyInfo {path, children, parents, theory, thms, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

343 
methods, data, ...}) => 
1291  344 
ThyInfo {path = path, children = children, parents = parents, 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

345 
thy_time = thy_time, ml_time = ml_time, 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

346 
theory = theory, thms = thms, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

347 
methods = methods, data = data} 
1291  348 
 None => error ("set_info: theory " ^ tname ^ " not found"); 
1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset

349 
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; 
391  350 

351 
(*Mark theory as changed since last read if it has been completly read *) 

559  352 
fun mark_outdated tname = 
971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset

353 
let val t = get_thyinfo tname; 
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset

354 
in if is_none t then () 
1291  355 
else 
356 
let val ThyInfo {thy_time, ml_time, ...} = the t 

357 
in set_info tname (if is_none thy_time then None else Some "") 

358 
(if is_none ml_time then None else Some "") 

359 
end 

971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset

360 
end; 
391  361 

1530  362 
(*Remove theorems associated with a theory from theory and theorem database*) 
363 
fun delete_thms tname = 

364 
let 

365 
val tinfo = case get_thyinfo tname of 

366 
Some (ThyInfo {path, children, parents, thy_time, ml_time, theory, 

367 
methods, data, ...}) => 

368 
ThyInfo {path = path, children = children, parents = parents, 

369 
thy_time = thy_time, ml_time = ml_time, 

370 
theory = theory, thms = Symtab.null, 

371 
methods = methods, data = data} 

1554  372 
 None => error ("Theory " ^ tname ^ " not stored by loader"); 
1530  373 

374 
val ThyInfo {theory, ...} = tinfo; 

375 
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys); 

376 
case theory of 

377 
Some t => delete_thm_db t 

378 
 None => () 

379 
end; 

380 

1291  381 
(*Make head of HTML dependency charts 
382 
Parameters are: 

383 
file: HTML file 

384 
tname: theory name 

385 
suffix: suffix of complementary chart 

386 
(sup if this head is for a subchart, sub if it is for a supchart; 

387 
empty for Pure and CPure subcharts) 

388 
gif_path: relative path to directory containing GIFs 

1313  389 
index_path: relative path to directory containing main theory chart 
1291  390 
*) 
1317  391 
fun mk_charthead file tname title repeats gif_path index_path package = 
1291  392 
output (file, 
393 
"<HTML><HEAD><TITLE>" ^ title ^ " of " ^ tname ^ 

394 
"</TITLE></HEAD>\n<H2>" ^ title ^ " of theory " ^ tname ^ 

395 
"</H2>\nThe name of every theory is linked to its theory file<BR>\n" ^ 

396 
"<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\ 

397 
\\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\ 

398 
\<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\ 

399 
\\" ALT = /\\></A> stands for supertheories (parent theories)\n" ^ 

1317  400 
(if not repeats then "" else 
401 
"<BR><TT>...</TT> stands for repeated subtrees") ^ 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

402 
"<P>\n<A HREF = \"" ^ tack_on index_path "index.html\ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

403 
\\">Back</A> to the index of " ^ package ^ "\n<HR>\n<PRE>"); 
1291  404 

405 
(*Convert .thy file to HTML and make chart of its supertheories*) 

406 
fun thyfile2html tpath tname = 

407 
let 

408 
val gif_path = relative_path tpath (!gif_path); 

1408  409 

410 
(*Determine name of current logic; if index_path is no subdirectory of 

411 
base_path then we take the last directory of index_path*) 

1317  412 
val package = 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

413 
if (!index_path) = "" then 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

414 
error "index_path is empty. Please use 'init_html()' instead of \ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

415 
\'make_html := true'" 
1408  416 
else if (!index_path) subdir_of (!base_path) then 
417 
relative_path (!base_path) (!index_path) 

1589
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

418 
else last_path (!index_path); 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

419 
val rel_index_path = relative_path tpath (!index_path); 
1291  420 

421 
(*Make list of all theories and all theories that own a .thy file*) 

422 
fun list_theories [] theories thy_files = (theories, thy_files) 

423 
 list_theories ((tname, ThyInfo {thy_time, ...}) :: ts) 

424 
theories thy_files = 

425 
list_theories ts (tname :: theories) 

426 
(if is_some thy_time andalso the thy_time <> "" then 

427 
tname :: thy_files 

428 
else thy_files); 

429 

430 
val (theories, thy_files) = 

431 
list_theories (Symtab.dest (!loaded_thys)) [] []; 

432 

433 
(*Do the conversion*) 

434 
fun gettext thy_file = 

435 
let 

436 
(*Convert special HTML characters ('&', '>', and '<')*) 

437 
val file = 

438 
explode (execute ("sed e 's/\\&/\\&/g' e 's/>/\\>/g' \ 

439 
\e 's/</\\</g' " ^ thy_file)); 

440 

441 
(*Isolate first (possibly nested) comment; 

442 
skip all leading whitespaces*) 

443 
val (comment, file') = 

444 
let fun first_comment ("*" :: ")" :: cs) co 1 = (co ^ "*)", cs) 

445 
 first_comment ("*" :: ")" :: cs) co d = 

446 
first_comment cs (co ^ "*)") (d1) 

447 
 first_comment ("(" :: "*" :: cs) co d = 

448 
first_comment cs (co ^ "(*") (d+1) 

449 
 first_comment (" " :: cs) "" 0 = first_comment cs "" 0 

450 
 first_comment ("\n" :: cs) "" 0 = first_comment cs "" 0 

451 
 first_comment ("\t" :: cs) "" 0 = first_comment cs "" 0 

452 
 first_comment cs "" 0 = ("", cs) 

453 
 first_comment (c :: cs) co d = 

454 
first_comment cs (co ^ implode [c]) d 

455 
 first_comment [] co _ = 

456 
error ("Unexpected end of file " ^ tname ^ ".thy."); 

457 
in first_comment file "" 0 end; 

458 

459 
(*Process line defining theory's ancestors; 

460 
convert valid theory names to links to their HTML file*) 

461 
val (ancestors, body) = 

462 
let 

463 
fun make_links l result = 

464 
let val (pre, letter) = take_prefix (not o is_letter) l; 

465 

466 
val (id, rest) = 

467 
take_prefix (is_quasi_letter orf is_digit) letter; 

468 

469 
val id = implode id; 

470 

471 
(*Make a HTML link out of a theory name*) 

472 
fun make_link t = 

473 
let val path = path_of t; 

474 
in "<A HREF = \"" ^ 

1323  475 
tack_on (relative_path tpath path) ("." ^ t) ^ 
1291  476 
".html\">" ^ t ^ "</A>" end; 
477 
in if not (id mem theories) then (result, implode l) 

478 
else if id mem thy_files then 

479 
make_links rest (result ^ implode pre ^ make_link id) 

480 
else make_links rest (result ^ implode pre ^ id) 

481 
end; 

482 

483 
val (pre, rest) = take_prefix (fn c => c <> "=") file'; 

484 

485 
val (ancestors, body) = 

486 
if null rest then 

487 
error ("Missing \"=\" in file " ^ tname ^ ".thy.\n\ 

488 
\(Make sure that the last line ends with a linebreak.)") 

489 
else 

490 
make_links rest ""; 

491 
in (implode pre ^ ancestors, body) end; 

492 
in "<HTML><HEAD><TITLE>" ^ tname ^ ".thy</TITLE></HEAD>\n\n<BODY>\n" ^ 

493 
"<H2>" ^ tname ^ ".thy</H2>\n<A HREF = \"" ^ 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

494 
tack_on rel_index_path "index.html\ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

495 
\\">Back</A> to the index of " ^ package ^ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

496 
"\n<HR>\n\n<PRE>\n" ^ comment ^ ancestors ^ body ^ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

497 
"</PRE>\n" 
1291  498 
end; 
499 

500 
(** Make chart of supertheories **) 

501 

1323  502 
val sup_out = open_out (tack_on tpath ("." ^ tname ^ "_sup.html")); 
503 
val sub_out = open_out (tack_on tpath ("." ^ tname ^ "_sub.html")); 

1291  504 

505 
(*Theories that already have been listed in this chart*) 

506 
val listed = ref []; 

507 

508 
val wanted_theories = 

509 
filter (fn s => s mem thy_files orelse s = "Pure" orelse s = "CPure") 

510 
theories; 

511 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

512 
(*Make tree of theory dependencies*) 
1291  513 
fun list_ancestors tname level continued = 
514 
let 

515 
fun mk_entry [] = () 

516 
 mk_entry (t::ts) = 

517 
let 

518 
val is_pure = t = "Pure" orelse t = "CPure"; 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

519 
val path = if is_pure then (the (!pure_subchart)) 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

520 
else path_of t; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

521 
val rel_path = relative_path tpath path; 
1403
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

522 
val repeated = t mem (!listed) andalso 
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

523 
not (null (parents_of_name t)); 
1291  524 

525 
fun mk_offset [] cur = 

526 
if level < cur then error "Error in mk_offset" 

527 
else implode (replicate (level  cur) " ") 

528 
 mk_offset (l::ls) cur = 

529 
implode (replicate (l  cur) " ") ^ " " ^ 

530 
mk_offset ls (l+1); 

531 
in output (sup_out, 

532 
" " ^ mk_offset continued 0 ^ 

1323  533 
"\\__" ^ (if is_pure then t else 
534 
"<A HREF=\"" ^ tack_on rel_path ("." ^ t) ^ 

535 
".html\">" ^ t ^ "</A>") ^ 

1317  536 
(if repeated then "..." else " ") ^ 
1323  537 
"<A HREF = \"" ^ tack_on rel_path ("." ^ t) ^ 
1317  538 
"_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ 
1291  539 
tack_on gif_path "red_arrow.gif\" ALT = \\/></A>" ^ 
540 
(if is_pure then "" 

1323  541 
else "<A HREF = \"" ^ tack_on rel_path ("." ^ t) ^ 
1317  542 
"_sup.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ 
1291  543 
tack_on gif_path "blue_arrow.gif\ 
1317  544 
\\" ALT = /\\></A>") ^ 
545 
"\n"); 

546 
if repeated then () 

547 
else (listed := t :: (!listed); 

1291  548 
list_ancestors t (level+1) (if null ts then continued 
549 
else continued @ [level]); 

550 
mk_entry ts) 

551 
end; 

552 

553 
val relatives = 

1403
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

554 
filter (fn s => s mem wanted_theories) (parents_of_name tname); 
1291  555 
in mk_entry relatives end; 
556 
in if is_some (!cur_htmlfile) then 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

557 
(close_out (the (!cur_htmlfile)); 
1580
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1554
diff
changeset

558 
warning "Last theory's HTML file has not been closed.") 
1291  559 
else (); 
1323  560 
cur_htmlfile := Some (open_out (tack_on tpath ("." ^ tname ^ ".html"))); 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

561 
cur_has_title := false; 
1291  562 
output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy")); 
563 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

564 
mk_charthead sup_out tname "Ancestors" true gif_path rel_index_path 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

565 
package; 
1291  566 
output(sup_out, 
1323  567 
"<A HREF=\"." ^ tname ^ ".html\">" ^ tname ^ "</A> \ 
568 
\<A HREF = \"." ^ tname ^ 

1317  569 
"_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ 
1291  570 
tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\n"); 
571 
list_ancestors tname 0 []; 

572 
output (sup_out, "</PRE><HR></BODY></HTML>"); 

573 
close_out sup_out; 

574 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

575 
mk_charthead sub_out tname "Children" false gif_path rel_index_path 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

576 
package; 
1291  577 
output(sub_out, 
1323  578 
"<A HREF=\"." ^ tname ^ ".html\">" ^ tname ^ "</A> \ 
579 
\<A HREF = \"." ^ tname ^ "_sup.html\"><IMG SRC = \"" ^ 

1317  580 
tack_on gif_path "blue_arrow.gif\" BORDER=0 ALT = \\/></A>\n"); 
1291  581 
close_out sub_out 
582 
end; 

583 

1603
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

584 
(*Invoke every put method stored in a theory's methods table to initialize 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

585 
the state of user defined variables*) 
1656  586 
fun put_thydata first tname = 
1603
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

587 
let val (methods, data) = 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

588 
case get_thyinfo tname of 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

589 
Some (ThyInfo {methods, data, ...}) => 
1656  590 
(methods, Symtab.dest ((if first then fst else snd) data)) 
1603
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

591 
 None => error ("Theory " ^ tname ^ " not stored by loader"); 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

592 

44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

593 
fun put_data (id, date) = 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

594 
case Symtab.lookup (methods, id) of 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

595 
Some (ThyMethods {put, ...}) => put date 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

596 
 None => error ("No method defined for theory data \"" ^ 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

597 
id ^ "\""); 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

598 
in seq put_data data end; 
1291  599 

1656  600 
val set_current_thy = put_thydata false; 
601 

559  602 
(*Read .thy and .ML files that haven't been read yet or have changed since 
391  603 
they were last read; 
559  604 
loaded_thys is a thy_info list ref containing all theories that have 
391  605 
completly been read by this and preceeding use_thy calls. 
1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

606 
tmp_loadpath is temporarily added to loadpath while the ancestors of a 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

607 
theory that the user specified as e.g. "ex/Nat" are loaded. Because of 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

608 
raised exceptions we cannot guarantee that it's value is always valid. 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

609 
Therefore this has to be assured by the first parameter of use_thy1 which 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

610 
is "true" if use_thy gets invoked by mk_base and "false" else. 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

611 
*) 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

612 
fun use_thy1 tmp_loadpath_valid name = 
1242  613 
let 
614 
val (path, tname) = split_filename name; 

1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

615 
val dummy = (tmp_loadpath := 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

616 
(if not tmp_loadpath_valid then (if path = "" then [] else [path]) 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

617 
else !tmp_loadpath)); 
1242  618 
val (thy_file, ml_file) = get_filenames path tname; 
619 
val (abs_path, _) = if thy_file = "" then split_filename ml_file 

620 
else split_filename thy_file; 

621 
val (thy_uptodate, ml_uptodate) = thy_unchanged tname thy_file ml_file; 

1403
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

622 
val old_parents = parents_of_name tname; 
391  623 

1242  624 
(*Set absolute path for loaded theory *) 
625 
fun set_path () = 

1291  626 
let val ThyInfo {children, parents, thy_time, ml_time, theory, thms, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

627 
methods, data, ...} = 
1242  628 
the (Symtab.lookup (!loaded_thys, tname)); 
629 
in loaded_thys := Symtab.update ((tname, 

1291  630 
ThyInfo {path = abs_path, 
631 
children = children, parents = parents, 

1242  632 
thy_time = thy_time, ml_time = ml_time, 
633 
theory = theory, thms = thms, 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

634 
methods = methods, data = data}), 
1242  635 
!loaded_thys) 
636 
end; 

637 

638 
(*Mark all direct descendants of a theory as changed *) 

639 
fun mark_children thy = 

1291  640 
let val children = children_of thy; 
1242  641 
val present = filter (is_some o get_thyinfo) children; 
642 
val loaded = filter already_loaded present; 

643 
in if loaded <> [] then 

644 
writeln ("The following children of theory " ^ (quote thy) 

645 
^ " are now outofdate: " 

646 
^ (quote (space_implode "\",\"" loaded))) 

647 
else (); 

648 
seq mark_outdated present 

649 
end; 

391  650 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

651 
(*Invoke every get method stored in the methods table and store result in 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

652 
data table*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

653 
fun save_data thy_only = 
1291  654 
let val ThyInfo {path, children, parents, thy_time, ml_time, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

655 
theory, thms, methods, data} = the (get_thyinfo tname); 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

656 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

657 
fun get_data [] data = data 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

658 
 get_data ((id, ThyMethods {get, ...}) :: ms) data = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

659 
get_data ms (Symtab.update ((id, get ()), data)); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

660 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

661 
val new_data = get_data (Symtab.dest methods) Symtab.null; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

662 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

663 
val data' = if thy_only then (new_data, snd data) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

664 
else (fst data, new_data); 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

665 
in loaded_thys := Symtab.update 
1291  666 
((tname, ThyInfo {path = path, 
667 
children = children, parents = parents, 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

668 
thy_time = thy_time, ml_time = ml_time, 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

669 
theory = theory, thms = thms, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

670 
methods = methods, data = data'}), 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

671 
!loaded_thys) 
1242  672 
end; 
673 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

674 
(*Add theory to file listing all loaded theories (for index.html) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

675 
and to the subcharts of its parents*) 
1480  676 
local exception MK_HTML in 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

677 
fun mk_html () = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

678 
let val new_parents = parents_of_name tname \\ old_parents; 
1291  679 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

680 
fun robust_seq (proc: 'a > unit) : 'a list > unit = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

681 
let fun seqf [] = () 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

682 
 seqf (x :: xs) = (proc x handle _ => (); seqf xs) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

683 
in seqf end; 
1291  684 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

685 
(*Add child to parents' subtheory charts*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

686 
fun add_to_parents t = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

687 
let val path = if t = "Pure" orelse t = "CPure" then 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

688 
(the (!pure_subchart)) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

689 
else path_of t; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

690 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

691 
val gif_path = relative_path path (!gif_path); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

692 
val rel_path = relative_path path abs_path; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

693 
val tpath = tack_on rel_path ("." ^ tname); 
1291  694 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

695 
val fname = tack_on path ("." ^ t ^ "_sub.html"); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

696 
val out = if file_exists fname then 
1602
699ad6611c1e
fixed incompatibility of add_to_parents with SML109's new Io exceptions
clasohm
parents:
1598
diff
changeset

697 
open_append fname handle e => 
699ad6611c1e
fixed incompatibility of add_to_parents with SML109's new Io exceptions
clasohm
parents:
1598
diff
changeset

698 
(warning ("Unable to write to file " ^ 
699ad6611c1e
fixed incompatibility of add_to_parents with SML109's new Io exceptions
clasohm
parents:
1598
diff
changeset

699 
fname); raise e) 
1480  700 
else raise MK_HTML; 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

701 
in output (out, 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

702 
" \n \\__<A HREF=\"" ^ 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

703 
tack_on rel_path ("." ^ tname) ^ ".html\">" ^ tname ^ 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

704 
"</A> <A HREF = \"" ^ tpath ^ "_sub.html\">\ 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

705 
\<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

706 
tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\ 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

707 
\<A HREF = \"" ^ tpath ^ "_sup.html\">\ 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

708 
\<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

709 
tack_on gif_path "blue_arrow.gif\" ALT = /\\></A>\n"); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

710 
close_out out 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

711 
end; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

712 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

713 
val theory_list = 
1589
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

714 
open_append (tack_on (!index_path) ".theory_list.txt") 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

715 
handle _ => (make_html := false; 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

716 
writeln ("Warning: Cannot write to " ^ 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

717 
(!index_path) ^ " while making HTML files.\n\ 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

718 
\HTML generation has been switched off.\n\ 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

719 
\Call init_html() from within a \ 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

720 
\writeable directory to reactivate it."); 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

721 
raise MK_HTML) 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

722 
in output (theory_list, tname ^ " " ^ abs_path ^ "\n"); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

723 
close_out theory_list; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

724 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

725 
robust_seq add_to_parents new_parents 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

726 
end 
1554  727 
end; 
728 

729 
(*Make sure that loaded_thys contains an entry for tname*) 

730 
fun init_thyinfo () = 

731 
let val tinfo = ThyInfo {path = "", children = [], parents = [], 

732 
thy_time = None, ml_time = None, 

733 
theory = None, thms = Symtab.null, 

734 
methods = Symtab.null, 

735 
data = (Symtab.null, Symtab.null)}; 

736 
in if is_some (get_thyinfo tname) then () 

737 
else loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) 

738 
end; 

1242  739 
in if thy_uptodate andalso ml_uptodate then () 
740 
else 

1386
cf066d9b4c4f
fixed bug: cur_thyname was overwritten because of early assignment
clasohm
parents:
1378
diff
changeset

741 
(if thy_file = "" then () 
1656  742 
else if thy_uptodate then put_thydata true tname 
391  743 
else 
1242  744 
(writeln ("Reading \"" ^ name ^ ".thy\""); 
1291  745 

1554  746 
init_thyinfo (); 
1530  747 
delete_thms tname; 
1242  748 
read_thy tname thy_file; 
749 
use (out_name tname); 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

750 
save_data true; 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

751 

1308  752 
(*Store axioms of theory 
753 
(but only if it's not a copy of an older theory)*) 

1403
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

754 
let val parents = parents_of_name tname; 
1308  755 
val this_thy = theory_of tname; 
756 
val axioms = 

757 
if length parents = 1 

758 
andalso Sign.eq_sg (sign_of (theory_of (hd parents)), 

759 
sign_of this_thy) then [] 

760 
else axioms_of this_thy; 

761 
in map store_thm_db axioms end; 

762 

1242  763 
if not (!delete_tmpfiles) then () 
1291  764 
else delete_file (out_name tname); 
765 

766 
if not (!make_html) then () 

767 
else thyfile2html abs_path tname 

1242  768 
); 
1386
cf066d9b4c4f
fixed bug: cur_thyname was overwritten because of early assignment
clasohm
parents:
1378
diff
changeset

769 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

770 
set_info tname (Some (file_info thy_file)) None; 
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

771 
(*mark thy_file as successfully loaded*) 
391  772 

1242  773 
if ml_file = "" then () 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

774 
else (writeln ("Reading \"" ^ name ^ ".ML\""); 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

775 
use ml_file); 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

776 
save_data false; 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

777 

8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

778 
(*Store theory again because it could have been redefined*) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

779 
use_string 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

780 
["val _ = store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"]; 
391  781 

1313  782 
(*Add theory to list of all loaded theories (for index.html) 
1291  783 
and add it to its parents' subcharts*) 
784 
if !make_html then 

785 
let val path = path_of tname; 

1589
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

786 
in if path = "" then (*first time theory has been read*) 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

787 
(mk_html() handle MK_HTML => ()) 
1291  788 
else () 
789 
end 

790 
else (); 

791 

1242  792 
(*Now set the correct info*) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

793 
set_info tname (Some (file_info thy_file)) (Some (file_info ml_file)); 
1242  794 
set_path (); 
795 

796 
(*Mark theories that have to be reloaded*) 

1291  797 
mark_children tname; 
798 

799 
(*Close HTML file*) 

800 
case !cur_htmlfile of 

801 
Some out => (output (out, "<HR></BODY></HTML>\n"); 

802 
close_out out; 

803 
cur_htmlfile := None) 

804 
 None => () 

1242  805 
) 
806 
end; 

391  807 

1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

808 
val use_thy = use_thy1 false; 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

809 

391  810 
fun time_use_thy tname = timeit(fn()=> 
559  811 
(writeln("\n**** Starting Theory " ^ tname ^ " ****"); 
391  812 
use_thy tname; 
813 
writeln("\n**** Finished Theory " ^ tname ^ " ****")) 

814 
); 

815 

816 
(*Load all thy or ML files that have been changed and also 

1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

817 
all theories that depend on them.*) 
391  818 
fun update () = 
1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

819 
let (*List theories in the order they have to be loaded in.*) 
391  820 
fun load_order [] result = result 
821 
 load_order thys result = 

1291  822 
let fun next_level [] = [] 
823 
 next_level (t :: ts) = 

824 
let val children = children_of t 

825 
in children union (next_level ts) end; 

559  826 

1291  827 
val descendants = next_level thys; 
828 
in load_order descendants ((result \\ descendants) @ descendants) 

829 
end; 

391  830 

831 
fun reload_changed (t :: ts) = 

1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

832 
let val abspath = case get_thyinfo t of 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

833 
Some (ThyInfo {path, ...}) => path 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

834 
 None => ""; 
391  835 

1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

836 
val (thy_file, ml_file) = get_filenames abspath t; 
391  837 
val (thy_uptodate, ml_uptodate) = 
838 
thy_unchanged t thy_file ml_file; 

839 
in if thy_uptodate andalso ml_uptodate then () 

840 
else use_thy t; 

841 
reload_changed ts 

842 
end 

843 
 reload_changed [] = (); 

844 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset

845 
(*Remove all theories that are no descendants of ProtoPure. 
391  846 
If there are still children in the deleted theory's list 
847 
schedule them for reloading *) 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

848 
fun collect_garbage no_garbage = 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

849 
let fun collect ((tname, ThyInfo {children, ...}) :: ts) = 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

850 
if tname mem no_garbage then collect ts 
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset

851 
else (writeln ("Theory \"" ^ tname ^ 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset

852 
"\" is no longer linked with ProtoPure  removing it."); 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

853 
remove_thy tname; 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

854 
seq mark_outdated children) 
391  855 
 collect [] = () 
559  856 
in collect (Symtab.dest (!loaded_thys)) end; 
1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

857 
in tmp_loadpath := []; 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

858 
collect_garbage ("ProtoPure" :: (load_order ["ProtoPure"] [])); 
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset

859 
reload_changed (load_order ["Pure", "CPure"] []) 
391  860 
end; 
861 

862 
(*Merge theories to build a base for a new theory. 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

863 
Base members are only loaded if they are missing.*) 
586
201e115d8031
renamed base_on into mk_base and moved it to the beginning of the generated
clasohm
parents:
559
diff
changeset

864 
fun mk_base bases child mk_draft = 
1291  865 
let (*Show the cycle that would be created by add_child*) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

866 
fun show_cycle base = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

867 
let fun find_it result curr = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

868 
let val tinfo = get_thyinfo curr 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

869 
in if base = curr then 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

870 
error ("Cyclic dependency of theories: " 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

871 
^ child ^ ">" ^ base ^ result) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

872 
else if is_some tinfo then 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

873 
let val ThyInfo {children, ...} = the tinfo 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

874 
in seq (find_it (">" ^ curr ^ result)) children 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

875 
end 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

876 
else () 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

877 
end 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

878 
in find_it "" child end; 
391  879 

1291  880 
(*Check if a cycle would be created by add_child*) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

881 
fun find_cycle base = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

882 
if base mem (get_descendants [child]) then show_cycle base 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

883 
else (); 
559  884 

1291  885 
(*Add child to child list of base*) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

886 
fun add_child base = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

887 
let val tinfo = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

888 
case Symtab.lookup (!loaded_thys, base) of 
1291  889 
Some (ThyInfo {path, children, parents, thy_time, ml_time, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

890 
theory, thms, methods, data}) => 
1291  891 
ThyInfo {path = path, 
892 
children = child ins children, parents = parents, 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

893 
thy_time = thy_time, ml_time = ml_time, 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

894 
theory = theory, thms = thms, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

895 
methods = methods, data = data} 
1291  896 
 None => ThyInfo {path = "", children = [child], parents = [], 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

897 
thy_time = None, ml_time = None, 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

898 
theory = None, thms = Symtab.null, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

899 
methods = Symtab.null, 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

900 
data = (Symtab.null, Symtab.null)}; 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

901 
in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end; 
559  902 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

903 
(*Load a base theory if not already done 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

904 
and no cycle would be created *) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

905 
fun load base = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

906 
let val thy_loaded = already_loaded base 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

907 
(*test this before child is added *) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

908 
in 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

909 
if child = base then 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

910 
error ("Cyclic dependency of theories: " ^ child 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

911 
^ ">" ^ child) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

912 
else 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

913 
(find_cycle base; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

914 
add_child base; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

915 
if thy_loaded then () 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

916 
else (writeln ("Autoloading theory " ^ (quote base) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

917 
^ " (used by " ^ (quote child) ^ ")"); 
1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

918 
use_thy1 true base) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

919 
) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

920 
end; 
391  921 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

922 
(*Load all needed files and make a list of all real theories *) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

923 
fun load_base (Thy b :: bs) = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

924 
(load b; 
1291  925 
b :: load_base bs) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

926 
 load_base (File b :: bs) = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

927 
(load b; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

928 
load_base bs) (*don't add it to mergelist *) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

929 
 load_base [] = []; 
391  930 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

931 
val dummy = unlink_thy child; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

932 
val mergelist = load_base bases; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

933 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

934 
val base_thy = (writeln ("Loading theory " ^ (quote child)); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

935 
merge_thy_list mk_draft (map theory_of mergelist)); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

936 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

937 
val datas = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

938 
let fun get_data t = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

939 
let val ThyInfo {data, ...} = the (get_thyinfo t) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

940 
in snd data end; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

941 
in map (Symtab.dest o get_data) mergelist end; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

942 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

943 
val methods = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

944 
let fun get_methods t = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

945 
let val ThyInfo {methods, ...} = the (get_thyinfo t) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

946 
in methods end; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

947 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

948 
val ms = map get_methods mergelist; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

949 
in if null ms then Symtab.null 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

950 
else foldl (Symtab.merge (fn (x,y) => true)) (hd ms, tl ms) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

951 
end; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

952 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

953 
(*merge two sorted association lists*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

954 
fun merge_two ([], d2) = d2 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

955 
 merge_two (d1, []) = d1 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

956 
 merge_two (l1 as ((p1 as (id1 : string, d1)) :: d1s), 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

957 
l2 as ((p2 as (id2, d2)) :: d2s)) = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

958 
if id1 < id2 then 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

959 
p1 :: merge_two (d1s, l2) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

960 
else 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

961 
p2 :: merge_two (l1, d2s); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

962 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

963 
(*Merge multiple occurence of data; also call put for each merged list*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

964 
fun merge_multi [] None = [] 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

965 
 merge_multi [] (Some (id, ds)) = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

966 
let val ThyMethods {merge, put, ...} = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

967 
the (Symtab.lookup (methods, id)); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

968 
in put (merge ds); [id] end 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

969 
 merge_multi ((id, d) :: ds) None = merge_multi ds (Some (id, [d])) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

970 
 merge_multi ((id, d) :: ds) (Some (id2, d2s)) = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

971 
if id = id2 then 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

972 
merge_multi ds (Some (id2, d :: d2s)) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

973 
else 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

974 
let val ThyMethods {merge, put, ...} = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

975 
the (Symtab.lookup (methods, id2)); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

976 
in put (merge d2s); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

977 
id2 :: merge_multi ds (Some (id, [d])) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

978 
end; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

979 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

980 
val merged = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

981 
if null datas then [] 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

982 
else merge_multi (foldl merge_two (hd datas, tl datas)) None; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

983 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

984 
val dummy = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

985 
let val unmerged = map fst (Symtab.dest methods) \\ merged; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

986 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

987 
fun put_empty id = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

988 
let val ThyMethods {merge, put, ...} = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

989 
the (Symtab.lookup (methods, id)); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

990 
in put (merge []) end; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

991 
in seq put_empty unmerged end; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

992 

1291  993 
val dummy = 
994 
let val tinfo = case Symtab.lookup (!loaded_thys, child) of 

995 
Some (ThyInfo {path, children, thy_time, ml_time, theory, thms, 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

996 
data, ...}) => 
1291  997 
ThyInfo {path = path, 
998 
children = children, parents = mergelist, 

999 
thy_time = thy_time, ml_time = ml_time, 

1000 
theory = theory, thms = thms, 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

1001 
methods = methods, data = data} 
1291  1002 
 None => error ("set_parents: theory " ^ child ^ " not found"); 
1003 
in loaded_thys := Symtab.update ((child, tinfo), !loaded_thys) end; 

1004 

1386
cf066d9b4c4f
fixed bug: cur_thyname was overwritten because of early assignment
clasohm
parents:
1378
diff
changeset

1005 
in cur_thyname := child; 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1006 
base_thy 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1007 
end; 
391  1008 

1291  1009 
(*Change theory object for an existent item of loaded_thys*) 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

1010 
fun store_theory (thy, tname) = 
559  1011 
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of 
1291  1012 
Some (ThyInfo {path, children, parents, thy_time, ml_time, thms, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

1013 
methods, data, ...}) => 
1291  1014 
ThyInfo {path = path, children = children, parents = parents, 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

1015 
thy_time = thy_time, ml_time = ml_time, 
1242  1016 
theory = Some thy, thms = thms, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

1017 
methods = methods, data = data} 
1291  1018 
 None => error ("store_theory: theory " ^ tname ^ " not found"); 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

1019 
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; 
559  1020 

1021 

1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset

1022 
(*** Store and retrieve theorems ***) 
1664  1023 
(*Guess the name of a theory object 
1024 
(First the quick way by looking at the stamps; if that doesn't work, 

1025 
we search loaded_thys for the first theory which fits.) 

1026 
*) 

1027 
fun thyname_of_sign sg = 

1028 
let val ref xname = hd (#stamps (Sign.rep_sg sg)); 

1029 
val opt_info = get_thyinfo xname; 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

1030 

559  1031 
fun eq_sg (ThyInfo {theory = None, ...}) = false 
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset

1032 
 eq_sg (ThyInfo {theory = Some thy, ...}) = Sign.eq_sg (sg,sign_of thy); 
559  1033 

1034 
val show_sg = Pretty.str_of o Sign.pretty_sg; 

1035 
in 

1664  1036 
if is_some opt_info andalso eq_sg (the opt_info) then xname 
559  1037 
else 
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1038 
(case Symtab.find_first (eq_sg o snd) (!loaded_thys) of 
1664  1039 
Some (name, _) => name 
559  1040 
 None => error ("Theory " ^ show_sg sg ^ " not stored by loader")) 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

1041 
end; 
391  1042 

1664  1043 
(*Guess to which theory a signature belongs and return it's thy_info*) 
1044 
fun thyinfo_of_sign sg = 

1045 
let val name = thyname_of_sign sg; 

1046 
in (name, the (get_thyinfo name)) end; 

1047 

559  1048 

715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset

1049 
(*Try to get the theory object corresponding to a given signature*) 
559  1050 
fun theory_of_sign sg = 
1051 
(case thyinfo_of_sign sg of 

1052 
(_, ThyInfo {theory = Some thy, ...}) => thy 

1053 
 _ => sys_error "theory_of_sign"); 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

1054 

715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset

1055 
(*Try to get the theory object corresponding to a given theorem*) 
559  1056 
val theory_of_thm = theory_of_sign o #sign o rep_thm; 
1057 

1058 

1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset

1059 
(** Store theorems **) 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

1060 

1538
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1061 
(*Makes HTML title for list of theorems; as this list may be empty and we 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1062 
don't want a title in that case, mk_theorems_title is only invoked when 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1063 
something is added to the list*) 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1064 
fun mk_theorems_title out = 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1065 
if not (!cur_has_title) then 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1066 
(cur_has_title := true; 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1067 
output (out, "<HR><H2>Theorems proved in <A HREF = \"" ^ 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1068 
(!cur_thyname) ^ ".ML\">" ^ (!cur_thyname) ^ 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1069 
".ML</A>:</H2>\n")) 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1070 
else (); 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1071 

1291  1072 
(*Store a theorem in the thy_info of its theory, 
1073 
and in the theory's HTML file*) 

559  1074 
fun store_thm (name, thm) = 
1075 
let 

1291  1076 
val (thy_name, ThyInfo {path, children, parents, thy_time, ml_time, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

1077 
theory, thms, methods, data}) = 
1529  1078 
thyinfo_of_sign (#sign (rep_thm thm)) 
1236
b54d51df9065
added check for duplicate theorems in theorem database;
clasohm
parents:
1223
diff
changeset

1079 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1080 
val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false) 
774
ea19f22ed23c
added warning for already stored theorem to store_thm
clasohm
parents:
759
diff
changeset

1081 
handle Symtab.DUPLICATE s => 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1082 
(if eq_thm (the (Symtab.lookup (thms, name)), thm) then 
1580
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1554
diff
changeset

1083 
(warning ("Theory database already contains copy of\ 
774
ea19f22ed23c
added warning for already stored theorem to store_thm
clasohm
parents:
759
diff
changeset

1084 
\ theorem " ^ quote name); 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1085 
(thms, true)) 
1236
b54d51df9065
added check for duplicate theorems in theorem database;
clasohm
parents:
1223
diff
changeset

1086 
else error ("Duplicate theorem name " ^ quote s 
b54d51df9065
added check for duplicate theorems in theorem database;
clasohm
parents:
1223
diff
changeset

1087 
^ " used in theory database")); 
1291  1088 

1089 
fun thm_to_html () = 

1090 
let fun escape [] = "" 

1091 
 escape ("<"::s) = "<" ^ escape s 

1092 
 escape (">"::s) = ">" ^ escape s 

1093 
 escape ("&"::s) = "&" ^ escape s 

1094 
 escape (c::s) = c ^ escape s; 

1095 
in case !cur_htmlfile of 

1096 
Some out => 

1538
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1097 
(mk_theorems_title out; 
2188  1098 
output (out, "<DD><EM>" ^ name ^ "</EM>\n<PRE>" ^ 
2030  1099 
escape 
1100 
(explode 

1101 
(string_of_thm (#1 (freeze_thaw thm)))) ^ 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1102 
"</PRE><P>\n") 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1103 
) 
1291  1104 
 None => () 
1105 
end; 

1529  1106 

1598
6f4d995590fd
For the new version of name_thm. Now the same theorem
paulson
parents:
1589
diff
changeset

1107 
(*Label this theorem*) 
6f4d995590fd
For the new version of name_thm. Now the same theorem
paulson
parents:
1589
diff
changeset

1108 
val thm' = Thm.name_thm (name, thm) 
559  1109 
in 
1110 
loaded_thys := Symtab.update 

1291  1111 
((thy_name, ThyInfo {path = path, children = children, parents = parents, 
1242  1112 
thy_time = thy_time, ml_time = ml_time, 
1113 
theory = theory, thms = thms', 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

1114 
methods = methods, data = data}), 
1242  1115 
!loaded_thys); 
1291  1116 
thm_to_html (); 
1529  1117 
if duplicate then thm' else store_thm_db (name, thm') 
559  1118 
end; 
1119 

715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset

1120 
(*Store result of proof in loaded_thys and as ML value*) 
758  1121 

1122 
val qed_thm = ref flexpair_def(*dummy*); 

1123 

1124 
fun bind_thm (name, thm) = 

1529  1125 
(qed_thm := store_thm (name, (standard thm)); 
1291  1126 
use_string ["val " ^ name ^ " = !qed_thm;"]); 
758  1127 

559  1128 
fun qed name = 
1529  1129 
(qed_thm := store_thm (name, result ()); 
1291  1130 
use_string ["val " ^ name ^ " = !qed_thm;"]); 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

1131 

746  1132 
fun qed_goal name thy agoal tacsf = 
1529  1133 
(qed_thm := store_thm (name, prove_goal thy agoal tacsf); 
1291  1134 
use_string ["val " ^ name ^ " = !qed_thm;"]); 
746  1135 

1136 
fun qed_goalw name thy rths agoal tacsf = 

1529  1137 
(qed_thm := store_thm (name, prove_goalw thy rths agoal tacsf); 
1291  1138 
use_string ["val " ^ name ^ " = !qed_thm;"]); 
559  1139 

783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1140 

1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset

1141 
(** Retrieve theorems **) 
559  1142 

783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1143 
(*Get all theorems belonging to a given theory*) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1144 
fun thmtab_of_thy thy = 
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1145 
let val (_, ThyInfo {thms, ...}) = thyinfo_of_sign (sign_of thy); 
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1146 
in thms end; 
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1147 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1148 
fun thmtab_of_name name = 
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1149 
let val ThyInfo {thms, ...} = the (get_thyinfo name); 
559  1150 
in thms end; 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

1151 

1598
6f4d995590fd
For the new version of name_thm. Now the same theorem
paulson
parents:
1589
diff
changeset

1152 
(*Get a stored theorem specified by theory and name. *) 
559  1153 
fun get_thm thy name = 
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1154 
let fun get [] [] searched = 
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1155 
raise THEORY ("get_thm: no theorem " ^ quote name, [thy]) 
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1156 
 get [] ng searched = 
871  1157 
get (ng \\ searched) [] searched 
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1158 
 get (t::ts) ng searched = 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1159 
(case Symtab.lookup (thmtab_of_name t, name) of 
1598
6f4d995590fd
For the new version of name_thm. Now the same theorem
paulson
parents:
1589
diff
changeset

1160 
Some thm => thm 
1403
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

1161 
 None => get ts (ng union (parents_of_name t)) (t::searched)); 
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1162 

08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1163 
val (tname, _) = thyinfo_of_sign (sign_of thy); 
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1164 
in get [tname] [] [] end; 
559  1165 

1529  1166 
(*Get stored theorems of a theory (original derivations) *) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1167 
val thms_of = Symtab.dest o thmtab_of_thy; 
559  1168 

778  1169 

1291  1170 

1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset

1171 

71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset

1172 
(*** Misc HTML functions ***) 
1291  1173 

1174 
(*Init HTML generator by setting paths and creating new files*) 

1175 
fun init_html () = 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1176 
let val cwd = pwd(); 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1177 

1323  1178 
val theory_list = close_out (open_out ".theory_list.txt"); 
1291  1179 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1180 
val rel_gif_path = relative_path cwd (!gif_path); 
1368  1181 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1182 
(*Make new HTML files for Pure and CPure*) 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1183 
fun init_pure_html () = 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1184 
let val pure_out = open_out ".Pure_sub.html"; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1185 
val cpure_out = open_out ".CPure_sub.html"; 
1408  1186 
val package = 
1187 
if cwd subdir_of (!base_path) then 

1188 
relative_path (!base_path) cwd 

1589
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

1189 
else last_path cwd; 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1190 
in mk_charthead pure_out "Pure" "Children" false rel_gif_path "" 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1191 
package; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1192 
mk_charthead cpure_out "CPure" "Children" false rel_gif_path "" 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1193 
package; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1194 
output (pure_out, "Pure\n"); 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1195 
output (cpure_out, "CPure\n"); 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1196 
close_out pure_out; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1197 
close_out cpure_out; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1198 
pure_subchart := Some cwd 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1199 
end; 
1291  1200 
in make_html := true; 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1201 
index_path := cwd; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1202 

1405
e9ca85a3713c
init_html now makes sure that base_path contains a physical path and no
clasohm
parents:
1403
diff
changeset

1203 
(*Make sure that base_path contains the physical path and no 
e9ca85a3713c
init_html now makes sure that base_path contains a physical path and no
clasohm
parents:
1403
diff
changeset

1204 
symbolic links*) 
e9ca85a3713c
init_html now makes sure that base_path contains a physical path and no
clasohm
parents:
1403
diff
changeset

1205 
cd (!base_path); 
e9ca85a3713c
init_html now makes sure that base_path contains a physical path and no
clasohm
parents:
1403
diff
changeset

1206 
base_path := pwd(); 
e9ca85a3713c
init_html now makes sure that base_path contains a physical path and no
clasohm
parents:
1403
diff
changeset

1207 
cd cwd; 
e9ca85a3713c
init_html now makes sure that base_path contains a physical path and no
clasohm
parents:
1403
diff
changeset

1208 

1408  1209 
if cwd subdir_of (!base_path) then () 
1580
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1554
diff
changeset

1210 
else warning "The current working directory seems to be no \ 
1408  1211 
\subdirectory of\nIsabelle's main directory. \ 
1212 
\Please ensure that base_path's value is correct.\n"; 

1405
e9ca85a3713c
init_html now makes sure that base_path contains a physical path and no
clasohm
parents:
1403
diff
changeset

1213 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1214 
writeln ("Setting path for index.html to " ^ quote cwd ^ 
1291  1215 
"\nGIF path has been set to " ^ quote (!gif_path)); 
1216 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1217 
if is_none (!pure_subchart) then init_pure_html() 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1218 
else () 
1291  1219 
end; 
1220 

1313  1221 
(*Generate index.html*) 
1368  1222 
fun finish_html () = if not (!make_html) then () else 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1223 
let val tlist_path = tack_on (!index_path) ".theory_list.txt"; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1224 
val theory_list = open_in tlist_path; 
1291  1225 
val theories = space_explode "\n" (input (theory_list, 999999)); 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1226 
val dummy = (close_in theory_list; delete_file tlist_path); 
1291  1227 

1313  1228 
val gif_path = relative_path (!index_path) (!gif_path); 
1291  1229 

1230 
(*Make entry for main chart of all theories.*) 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1231 
fun main_entry t = 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1232 
let 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1233 
val (name, path) = take_prefix (not_equal " ") (explode t); 
1291  1234 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1235 
val tname = implode name 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1236 
val tpath = tack_on (relative_path (!index_path) (implode (tl path))) 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1237 
("." ^ tname); 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1238 
in "<A HREF = \"" ^ tpath ^ "_sub.html\"><IMG SRC = \"" ^ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1239 
tack_on gif_path "red_arrow.gif\" BORDER=0 ALT = \\/></A>" ^ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1240 
"<A HREF = \"" ^ tpath ^ "_sup.html\"><IMG SRC = \"" ^ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1241 
tack_on gif_path "blue_arrow.gif\ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1242 
\\" BORDER=0 ALT = /\\></A> <A HREF = \"" ^ tpath ^ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1243 
".html\">" ^ tname ^ "</A><BR>\n" 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1244 
end; 
1291  1245 

1313  1246 
val out = open_out (tack_on (!index_path) "index.html"); 
1408  1247 

1248 
(*Find out in which subdirectory of Isabelle's main directory the 

1249 
index.html is placed; if index_path is no subdirectory of base_path 

1250 
then take the last directory of index_path*) 

1251 
val inside_isabelle = (!index_path) subdir_of (!base_path); 

1252 
val subdir = 

1253 
if inside_isabelle then relative_path (!base_path) (!index_path) 

1589
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

1254 
else last_path (!index_path); 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1255 
val subdirs = space_explode "/" subdir; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1256 

1408  1257 
(*Look for index.html in superdirectories; stop when Isabelle's 
1258 
main directory is reached*) 

1378  1259 
fun find_super_index [] n = ("", n) 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1260 
 find_super_index (p::ps) n = 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1261 
let val index_path = "/" ^ space_implode "/" (rev ps); 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1262 
in if file_exists (index_path ^ "/index.html") then (index_path, n) 
1408  1263 
else if length subdirs  n >= 0 then find_super_index ps (n+1) 
1264 
else ("", n) 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1265 
end; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1266 
val (super_index, level_diff) = 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1267 
find_super_index (rev (space_explode "/" (!index_path))) 1; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1268 
val level = length subdirs  level_diff; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1269 

b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1270 
(*Add link to current directory to 'super' index.html*) 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1271 
fun link_directory () = 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1272 
let val old_index = open_in (super_index ^ "/index.html"); 
