author  berghofe 
Fri, 15 Mar 1996 12:01:19 +0100  
changeset 1580  e3fd931e6095 
parent 1554  4ee99a973be4 
child 1589  fd6a571cb2b0 
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 
1291  74 

559  75 
val store_thm: string * thm > thm 
758  76 
val bind_thm: string * thm > unit 
559  77 
val qed: string > unit 
758  78 
val qed_thm: thm ref 
746  79 
val qed_goal: string > theory > string > (thm list > tactic list) > unit 
80 
val qed_goalw: string > theory>thm list>string>(thm list>tactic list) 

81 
> unit 

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

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

83 
val thms_of : theory > (string * thm) list 
1530  84 
val delete_thms : string > unit 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

85 

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

86 
val add_thydata : theory > string * thy_methods > unit 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

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

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

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

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

91 

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

92 
val print_theory : theory > unit 
1291  93 

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

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

95 
val gif_path : string ref 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

96 
val index_path : string ref 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

97 
val pure_subchart : string option ref 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

98 
val make_html : bool ref 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

99 
val init_html : unit > unit 
1368  100 
val finish_html : unit > unit 
1538
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

101 
val section : string > unit 
391  102 
end; 
103 

104 

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

105 
functor ReadthyFun(structure ThySyn: THY_SYN and ThmDB: THMDB): READTHY = 
391  106 
struct 
1242  107 

108 
open ThmDB Simplifier; 

391  109 

110 
datatype basetype = Thy of string 

111 
 File of string; 

112 

1291  113 
val loaded_thys = 
114 
ref (Symtab.make [("ProtoPure", 

115 
ThyInfo {path = "", 

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

117 
thy_time = Some "", ml_time = Some "", 

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

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

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

120 
data = (Symtab.null, Symtab.null)}), 
1291  121 
("Pure", 
122 
ThyInfo {path = "", children = [], 

123 
parents = ["ProtoPure"], 

124 
thy_time = Some "", ml_time = Some "", 

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

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

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

127 
data = (Symtab.null, Symtab.null)}), 
1291  128 
("CPure", 
129 
ThyInfo {path = "", 

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

131 
thy_time = Some "", ml_time = Some "", 

132 
theory = Some cpure_thy, 

133 
thms = Symtab.null, 

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

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

135 
data = (Symtab.null, Symtab.null)}) 
1291  136 
]); 
391  137 

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

138 
(*Default search path for theory files*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

139 
val loadpath = ref ["."]; 
1291  140 

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

141 
(*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

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

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

144 

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

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

146 
val delete_tmpfiles = ref true; 
1291  147 

391  148 

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

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

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

153 
structures inherit this value.) 

154 
*) 

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

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

157 
"Tools"); 

158 

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

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

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

161 
"/" ^ 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

162 

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

163 

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

164 
(** HTML variables **) 
1291  165 

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

166 
(*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

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

168 

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

169 
(*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

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

171 

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

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

173 
val make_html = ref false; 
1291  174 

175 
(*HTML file of theory currently being read 

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

177 
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

178 

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

179 
(*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

180 
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

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

182 

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

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

184 
val cur_thyname = 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 

391  187 

188 
(*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

189 
fun out_name tname = "." ^ tname ^ ".thy.ML"; 
391  190 

191 
(*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

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

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

197 
output (outstream, ThySyn.parse tname (input (instream, 999999))); 
391  198 
close_out outstream; 
199 
close_in instream 

200 
end; 

201 

1480  202 
fun file_exists file = (file_info file <> ""); 
391  203 

204 
(*Get thy_info for a loaded theory *) 

559  205 
fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname); 
391  206 

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

207 
(*Check if a theory was completly loaded *) 
391  208 
fun already_loaded thy = 
209 
let val t = get_thyinfo thy 

210 
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

211 
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

212 
in is_some thy_time andalso is_some ml_time end 
391  213 
end; 
214 

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

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

559  217 
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

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

219 
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

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

221 
val mn = is_none ml_time 
391  222 
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

223 
((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

224 
(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

225 
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

226 
(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

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

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

230 
 None => (false, false) 
391  231 

1291  232 
(*Get all direct descendants of a theory*) 
233 
fun children_of t = 

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

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

235 
 None => []; 
1291  236 

1242  237 
(*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

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

240 
 None => []; 
1242  241 

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

242 
(*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

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

244 
 get_descendants (t :: ts) = 
1291  245 
let val children = children_of t 
246 
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

247 

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

250 
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

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

252 
" not stored by loader"); 
1242  253 

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

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

257 
in path end; 

258 

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

261 
fun find_file "" name = 

1291  262 
let fun find_it (cur :: paths) = 
263 
if file_exists (tack_on cur name) then 

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

559  265 
else 
1291  266 
find_it paths 
391  267 
 find_it [] = "" 
268 
in find_it (!loadpath) end 

269 
 find_file path name = 

270 
if file_exists (tack_on path name) then tack_on path name 

271 
else ""; 

272 

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

274 
fun get_filenames path name = 

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

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

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

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

278 
val thy_file = absolute_path found; 
391  279 
val (thy_path, _) = split_filename thy_file; 
280 
val found = find_file path (name ^ ".ML"); 

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

281 
val ml_file = if thy_file = "" then absolute_path found 
391  282 
else if file_exists (tack_on thy_path (name ^ ".ML")) 
283 
then tack_on thy_path (name ^ ".ML") 

284 
else ""; 

285 
val searched_dirs = if path = "" then (!loadpath) else [path] 

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

287 
error ("Could not find file \"" ^ name ^ ".thy\" or \"" 

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

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

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

291 
else (); 

559  292 
(thy_file, ml_file) 
391  293 
end; 
294 

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

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

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

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

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

301 
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

302 
(warning ("File \"" ^ (tack_on path name) 
391  303 
^ ".thy\"\ncontaining theory \"" ^ name 
304 
^ "\" no longer exists."); 

305 
new_filename () 

306 
) 

307 
else (thy_file, ml_file) 

308 
end 

309 
else new_filename () 

310 
end; 

311 

312 
(*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

313 
fun unlink_thy tname = 
1291  314 
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

315 
theory, thms, methods, data}) = 
1291  316 
ThyInfo {path = path, children = children \ tname, parents = parents, 
1242  317 
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

318 
thms = thms, methods = methods, data = data} 
559  319 
in loaded_thys := Symtab.map remove (!loaded_thys) end; 
391  320 

321 
(*Remove a theory from loaded_thys *) 

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

322 
fun remove_thy tname = 
559  323 
loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname) 
324 
(Symtab.dest (!loaded_thys))); 

391  325 

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

326 
(*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

327 
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

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

330 
methods, data, ...}) => 
1291  331 
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

332 
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

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

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

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

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

559  339 
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

340 
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

341 
in if is_none t then () 
1291  342 
else 
343 
let val ThyInfo {thy_time, ml_time, ...} = the t 

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

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

346 
end 

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

347 
end; 
391  348 

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

351 
let 

352 
val tinfo = case get_thyinfo tname of 

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

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

355 
ThyInfo {path = path, children = children, parents = parents, 

356 
thy_time = thy_time, ml_time = ml_time, 

357 
theory = theory, thms = Symtab.null, 

358 
methods = methods, data = data} 

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

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

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

363 
case theory of 

364 
Some t => delete_thm_db t 

365 
 None => () 

366 
end; 

367 

1291  368 
(*Make head of HTML dependency charts 
369 
Parameters are: 

370 
file: HTML file 

371 
tname: theory name 

372 
suffix: suffix of complementary chart 

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

374 
empty for Pure and CPure subcharts) 

375 
gif_path: relative path to directory containing GIFs 

1313  376 
index_path: relative path to directory containing main theory chart 
1291  377 
*) 
1317  378 
fun mk_charthead file tname title repeats gif_path index_path package = 
1291  379 
output (file, 
380 
"<HTML><HEAD><TITLE>" ^ title ^ " of " ^ tname ^ 

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

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

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

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

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

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

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

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

389 
"<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

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

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

393 
fun thyfile2html tpath tname = 

394 
let 

395 
val gif_path = relative_path tpath (!gif_path); 

1408  396 

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

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

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

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

401 
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

402 
\'make_html := true'" 
1408  403 
else if (!index_path) subdir_of (!base_path) then 
404 
relative_path (!base_path) (!index_path) 

405 
else 

406 
last_elem (space_explode "/" (!index_path)); 

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

407 
val rel_index_path = relative_path tpath (!index_path); 
1291  408 

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

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

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

412 
theories thy_files = 

413 
list_theories ts (tname :: theories) 

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

415 
tname :: thy_files 

416 
else thy_files); 

417 

418 
val (theories, thy_files) = 

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

420 

421 
(*Do the conversion*) 

422 
fun gettext thy_file = 

423 
let 

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

425 
val file = 

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

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

428 

429 
(*Isolate first (possibly nested) comment; 

430 
skip all leading whitespaces*) 

431 
val (comment, file') = 

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

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

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

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

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

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

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

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

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

441 
 first_comment (c :: cs) co d = 

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

443 
 first_comment [] co _ = 

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

445 
in first_comment file "" 0 end; 

446 

447 
(*Process line defining theory's ancestors; 

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

449 
val (ancestors, body) = 

450 
let 

451 
fun make_links l result = 

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

453 

454 
val (id, rest) = 

455 
take_prefix (is_quasi_letter orf is_digit) letter; 

456 

457 
val id = implode id; 

458 

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

460 
fun make_link t = 

461 
let val path = path_of t; 

462 
in "<A HREF = \"" ^ 

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

466 
else if id mem thy_files then 

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

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

469 
end; 

470 

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

472 

473 
val (ancestors, body) = 

474 
if null rest then 

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

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

477 
else 

478 
make_links rest ""; 

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

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

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

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

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

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

484 
"\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

485 
"</PRE>\n" 
1291  486 
end; 
487 

488 
(** Make chart of supertheories **) 

489 

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

1291  492 

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

494 
val listed = ref []; 

495 

496 
val wanted_theories = 

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

498 
theories; 

499 

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

500 
(*Make tree of theory dependencies*) 
1291  501 
fun list_ancestors tname level continued = 
502 
let 

503 
fun mk_entry [] = () 

504 
 mk_entry (t::ts) = 

505 
let 

506 
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

507 
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

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

509 
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

510 
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

511 
not (null (parents_of_name t)); 
1291  512 

513 
fun mk_offset [] cur = 

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

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

516 
 mk_offset (l::ls) cur = 

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

518 
mk_offset ls (l+1); 

519 
in output (sup_out, 

520 
" " ^ mk_offset continued 0 ^ 

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

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

1317  524 
(if repeated then "..." else " ") ^ 
1323  525 
"<A HREF = \"" ^ tack_on rel_path ("." ^ t) ^ 
1317  526 
"_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ 
1291  527 
tack_on gif_path "red_arrow.gif\" ALT = \\/></A>" ^ 
528 
(if is_pure then "" 

1323  529 
else "<A HREF = \"" ^ tack_on rel_path ("." ^ t) ^ 
1317  530 
"_sup.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ 
1291  531 
tack_on gif_path "blue_arrow.gif\ 
1317  532 
\\" ALT = /\\></A>") ^ 
533 
"\n"); 

534 
if repeated then () 

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

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

538 
mk_entry ts) 

539 
end; 

540 

541 
val relatives = 

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

542 
filter (fn s => s mem wanted_theories) (parents_of_name tname); 
1291  543 
in mk_entry relatives end; 
544 
in if is_some (!cur_htmlfile) then 

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

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

546 
warning "Last theory's HTML file has not been closed.") 
1291  547 
else (); 
1323  548 
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

549 
cur_has_title := false; 
1291  550 
output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy")); 
551 

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

552 
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

553 
package; 
1291  554 
output(sup_out, 
1323  555 
"<A HREF=\"." ^ tname ^ ".html\">" ^ tname ^ "</A> \ 
556 
\<A HREF = \"." ^ tname ^ 

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

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

561 
close_out sup_out; 

562 

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

563 
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

564 
package; 
1291  565 
output(sub_out, 
1323  566 
"<A HREF=\"." ^ tname ^ ".html\">" ^ tname ^ "</A> \ 
567 
\<A HREF = \"." ^ tname ^ "_sup.html\"><IMG SRC = \"" ^ 

1317  568 
tack_on gif_path "blue_arrow.gif\" BORDER=0 ALT = \\/></A>\n"); 
1291  569 
close_out sub_out 
570 
end; 

571 

572 

559  573 
(*Read .thy and .ML files that haven't been read yet or have changed since 
391  574 
they were last read; 
559  575 
loaded_thys is a thy_info list ref containing all theories that have 
391  576 
completly been read by this and preceeding use_thy calls. 
577 
If a theory changed since its last use its children are marked as changed *) 

578 
fun use_thy name = 

1242  579 
let 
580 
val (path, tname) = split_filename name; 

581 
val (thy_file, ml_file) = get_filenames path tname; 

582 
val (abs_path, _) = if thy_file = "" then split_filename ml_file 

583 
else split_filename thy_file; 

584 
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

585 
val old_parents = parents_of_name tname; 
391  586 

1242  587 
(*Set absolute path for loaded theory *) 
588 
fun set_path () = 

1291  589 
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

590 
methods, data, ...} = 
1242  591 
the (Symtab.lookup (!loaded_thys, tname)); 
592 
in loaded_thys := Symtab.update ((tname, 

1291  593 
ThyInfo {path = abs_path, 
594 
children = children, parents = parents, 

1242  595 
thy_time = thy_time, ml_time = ml_time, 
596 
theory = theory, thms = thms, 

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

597 
methods = methods, data = data}), 
1242  598 
!loaded_thys) 
599 
end; 

600 

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

602 
fun mark_children thy = 

1291  603 
let val children = children_of thy; 
1242  604 
val present = filter (is_some o get_thyinfo) children; 
605 
val loaded = filter already_loaded present; 

606 
in if loaded <> [] then 

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

608 
^ " are now outofdate: " 

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

610 
else (); 

611 
seq mark_outdated present 

612 
end; 

391  613 

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

614 
(*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

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

616 
fun save_data thy_only = 
1291  617 
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

618 
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

619 

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

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

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

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

623 

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

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

625 

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

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

627 
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

628 
in loaded_thys := Symtab.update 
1291  629 
((tname, ThyInfo {path = path, 
630 
children = children, parents = parents, 

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

631 
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

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

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

634 
!loaded_thys) 
1242  635 
end; 
636 

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

637 
(*Invoke every put method stored in the methods table to initialize 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

638 
the state of user defined variables*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

639 
fun init_data methods data = 
1514
3e262b1c0b6c
fixed bug in init_data (put was only invoked for the first date)
clasohm
parents:
1483
diff
changeset

640 
let fun put_data (id, date) = 
3e262b1c0b6c
fixed bug in init_data (put was only invoked for the first date)
clasohm
parents:
1483
diff
changeset

641 
case Symtab.lookup (methods, id) of 
3e262b1c0b6c
fixed bug in init_data (put was only invoked for the first date)
clasohm
parents:
1483
diff
changeset

642 
Some (ThyMethods {put, ...}) => put date 
3e262b1c0b6c
fixed bug in init_data (put was only invoked for the first date)
clasohm
parents:
1483
diff
changeset

643 
 None => error ("No method defined for theory data \"" ^ 
3e262b1c0b6c
fixed bug in init_data (put was only invoked for the first date)
clasohm
parents:
1483
diff
changeset

644 
id ^ "\""); 
3e262b1c0b6c
fixed bug in init_data (put was only invoked for the first date)
clasohm
parents:
1483
diff
changeset

645 
in seq put_data data end; 
1291  646 

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

647 
(*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

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

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

651 
let val new_parents = parents_of_name tname \\ old_parents; 
1291  652 

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

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

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

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

656 
in seqf end; 
1291  657 

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

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

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

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

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

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

663 

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

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

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

666 
val tpath = tack_on rel_path ("." ^ tname); 
1291  667 

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

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

669 
val out = if file_exists fname then 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

670 
open_append fname handle Io s => 
1580
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1554
diff
changeset

671 
(warning ("Unable to write to file ." ^ 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

672 
fname); raise Io s) 
1480  673 
else raise MK_HTML; 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

685 

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

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

687 
open_append (tack_on (!index_path) ".theory_list.txt"); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

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

689 
close_out theory_list; 
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 
robust_seq add_to_parents new_parents 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

692 
end 
1554  693 
end; 
694 

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

696 
fun init_thyinfo () = 

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

698 
thy_time = None, ml_time = None, 

699 
theory = None, thms = Symtab.null, 

700 
methods = Symtab.null, 

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

702 
in if is_some (get_thyinfo tname) then () 

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

704 
end; 

1242  705 
in if thy_uptodate andalso ml_uptodate then () 
706 
else 

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

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

708 
else if thy_uptodate then 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

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

710 
in init_data methods (Symtab.dest (fst data)) end 
391  711 
else 
1242  712 
(writeln ("Reading \"" ^ name ^ ".thy\""); 
1291  713 

1554  714 
init_thyinfo (); 
1530  715 
delete_thms tname; 
1242  716 
read_thy tname thy_file; 
717 
use (out_name tname); 

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

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

719 

1308  720 
(*Store axioms of theory 
721 
(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

722 
let val parents = parents_of_name tname; 
1308  723 
val this_thy = theory_of tname; 
724 
val axioms = 

725 
if length parents = 1 

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

727 
sign_of this_thy) then [] 

728 
else axioms_of this_thy; 

729 
in map store_thm_db axioms end; 

730 

1242  731 
if not (!delete_tmpfiles) then () 
1291  732 
else delete_file (out_name tname); 
733 

734 
if not (!make_html) then () 

735 
else thyfile2html abs_path tname 

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

737 

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

738 
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

739 
(*mark thy_file as successfully loaded*) 
391  740 

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

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

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

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

745 

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

746 
(*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

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

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

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

753 
let val path = path_of tname; 

754 
in if path = "" then mk_html () (*first time theory has been read*) 

755 
else () 

756 
end 

757 
else (); 

758 

1242  759 
(*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

760 
set_info tname (Some (file_info thy_file)) (Some (file_info ml_file)); 
1242  761 
set_path (); 
762 

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

1291  764 
mark_children tname; 
765 

766 
(*Close HTML file*) 

767 
case !cur_htmlfile of 

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

769 
close_out out; 

770 
cur_htmlfile := None) 

771 
 None => () 

1242  772 
) 
773 
end; 

391  774 

775 
fun time_use_thy tname = timeit(fn()=> 

559  776 
(writeln("\n**** Starting Theory " ^ tname ^ " ****"); 
391  777 
use_thy tname; 
778 
writeln("\n**** Finished Theory " ^ tname ^ " ****")) 

779 
); 

780 

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

782 
all theories that depend on them *) 

783 
fun update () = 

784 
let (*List theories in the order they have to be loaded *) 

785 
fun load_order [] result = result 

786 
 load_order thys result = 

1291  787 
let fun next_level [] = [] 
788 
 next_level (t :: ts) = 

789 
let val children = children_of t 

790 
in children union (next_level ts) end; 

559  791 

1291  792 
val descendants = next_level thys; 
793 
in load_order descendants ((result \\ descendants) @ descendants) 

794 
end; 

391  795 

796 
fun reload_changed (t :: ts) = 

1291  797 
let fun abspath () = case get_thyinfo t of 
798 
Some (ThyInfo {path, ...}) => path 

799 
 None => ""; 

391  800 

801 
val (thy_file, ml_file) = get_filenames (abspath ()) t; 

802 
val (thy_uptodate, ml_uptodate) = 

803 
thy_unchanged t thy_file ml_file; 

804 
in if thy_uptodate andalso ml_uptodate then () 

805 
else use_thy t; 

806 
reload_changed ts 

807 
end 

808 
 reload_changed [] = (); 

809 

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

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

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

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

814 
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

815 
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

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

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

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

819 
seq mark_outdated children) 
391  820 
 collect [] = () 
559  821 
in collect (Symtab.dest (!loaded_thys)) end; 
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset

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

823 
reload_changed (load_order ["Pure", "CPure"] []) 
391  824 
end; 
825 

826 
(*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

827 
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

828 
fun mk_base bases child mk_draft = 
1291  829 
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

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

831 
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

832 
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

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

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

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

836 
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

837 
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

838 
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

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

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

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

842 
in find_it "" child end; 
391  843 

1291  844 
(*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

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

846 
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

847 
else (); 
559  848 

1291  849 
(*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

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

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

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

854 
theory, thms, methods, data}) => 
1291  855 
ThyInfo {path = path, 
856 
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

857 
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

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

859 
methods = methods, data = data} 
1291  860 
 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

861 
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

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

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

864 
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

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

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

867 
(*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

868 
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

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

870 
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

871 
(*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

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

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

874 
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

875 
^ ">" ^ child) 
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 
(find_cycle base; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

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

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

880 
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

881 
^ " (used by " ^ (quote child) ^ ")"); 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

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

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

884 
end; 
391  885 

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

886 
(*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

887 
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

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

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

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

892 
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

893 
 load_base [] = []; 
391  894 

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

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

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

897 

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

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

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

900 

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

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

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

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

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

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

906 

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

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

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

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

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

911 

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

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

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

914 
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

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

916 

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

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

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

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

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

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

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

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

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

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

926 

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

927 
(*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

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

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

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

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

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

933 
 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

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

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

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

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

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

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

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

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

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

943 

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

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

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

946 
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

947 

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

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

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

950 

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

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

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

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

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

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

956 

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

959 
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

960 
data, ...}) => 
1291  961 
ThyInfo {path = path, 
962 
children = children, parents = mergelist, 

963 
thy_time = thy_time, ml_time = ml_time, 

964 
theory = theory, thms = thms, 

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

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

968 

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

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

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

971 
end; 
391  972 

1291  973 
(*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

974 
fun store_theory (thy, tname) = 
559  975 
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of 
1291  976 
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

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

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

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

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

985 

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

986 
(*** Store and retrieve theorems ***) 
559  987 

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

988 
(*Guess to which theory a signature belongs and return it's thy_info*) 
559  989 
fun thyinfo_of_sign sg = 
990 
let 

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

992 
val opt_info = get_thyinfo xname; 

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

993 

559  994 
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

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

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

998 
in 

999 
if is_some opt_info andalso eq_sg (the opt_info) then 

1000 
(xname, the opt_info) 

1001 
else 

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

1002 
(case Symtab.find_first (eq_sg o snd) (!loaded_thys) of 
559  1003 
Some name_info => name_info 
1004 
 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

1005 
end; 
391  1006 

559  1007 

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

1008 
(*Try to get the theory object corresponding to a given signature*) 
559  1009 
fun theory_of_sign sg = 
1010 
(case thyinfo_of_sign sg of 

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

1012 
 _ => sys_error "theory_of_sign"); 

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

1013 

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

1014 
(*Try to get the theory object corresponding to a given theorem*) 
559  1015 
val theory_of_thm = theory_of_sign o #sign o rep_thm; 
1016 

1017 

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

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

1019 

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

1020 
(*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

1021 
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

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

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

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

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

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

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

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

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

1030 

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

559  1033 
fun store_thm (name, thm) = 
1034 
let 

1291  1035 
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

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

1038 

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

1039 
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

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

1041 
(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

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

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

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

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

1046 
^ " used in theory database")); 
1291  1047 

1048 
fun thm_to_html () = 

1049 
let fun escape [] = "" 

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

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

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

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

1054 
in case !cur_htmlfile of 

1055 
Some out => 

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

1056 
(mk_theorems_title out; 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1057 
output (out, "<EM>" ^ name ^ "</EM>\n<PRE>" ^ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1058 
escape (explode (string_of_thm (freeze thm))) ^ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

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

1060 
) 
1291  1061 
 None => () 
1062 
end; 

1529  1063 

1064 
(*Return version with trivial proof object; store original version *) 

1065 
val thm' = Thm.name_thm (the theory, name, thm) handle OPTION _ => thm 

559  1066 
in 
1067 
loaded_thys := Symtab.update 

1291  1068 
((thy_name, ThyInfo {path = path, children = children, parents = parents, 
1242  1069 
thy_time = thy_time, ml_time = ml_time, 
1070 
theory = theory, thms = thms', 

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

1071 
methods = methods, data = data}), 
1242  1072 
!loaded_thys); 
1291  1073 
thm_to_html (); 
1529  1074 
if duplicate then thm' else store_thm_db (name, thm') 
559  1075 
end; 
1076 

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

1077 
(*Store result of proof in loaded_thys and as ML value*) 
758  1078 

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

1080 

1081 
fun bind_thm (name, thm) = 

1529  1082 
(qed_thm := store_thm (name, (standard thm)); 
1291  1083 
use_string ["val " ^ name ^ " = !qed_thm;"]); 
758  1084 

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

1088 

746  1089 
fun qed_goal name thy agoal tacsf = 
1529  1090 
(qed_thm := store_thm (name, prove_goal thy agoal tacsf); 
1291  1091 
use_string ["val " ^ name ^ " = !qed_thm;"]); 
746  1092 

1093 
fun qed_goalw name thy rths agoal tacsf = 

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

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

1097 

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

1098 
(** Retrieve theorems **) 
559  1099 

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

1100 
(*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

1101 
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

1102 
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

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

1104 

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

1105 
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

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

1108 

1529  1109 
(*Get a stored theorem specified by theory and name. 
1110 
Derivation has the form Theorem(thy,name). *) 

559  1111 
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

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

1113 
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

1114 
 get [] ng searched = 
871  1115 
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

1116 
 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

1117 
(case Symtab.lookup (thmtab_of_name t, name) of 
1529  1118 
Some thm => Thm.name_thm(thy,name,thm) 
1403
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

1119 
 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

1120 

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

1121 
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

1122 
in get [tname] [] [] end; 
559  1123 

1529  1124 
(*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

1125 
val thms_of = Symtab.dest o thmtab_of_thy; 
559  1126 

778  1127 

1291  1128 

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

1129 

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

1130 
(*** Misc HTML functions ***) 
1291  1131 

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

1133 
fun init_html () = 

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

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

1135 

1323  1136 
val theory_list = close_out (open_out ".theory_list.txt"); 
1291  1137 

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

1138 
val rel_gif_path = relative_path cwd (!gif_path); 
1368  1139 

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

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

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

1142 
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

1143 
val cpure_out = open_out ".CPure_sub.html"; 
1408  1144 
val package = 
1145 
if cwd subdir_of (!base_path) then 

1146 
relative_path (!base_path) cwd 

1147 
else 

1148 
last_elem (space_explode "/" cwd); 

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

1149 
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

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

1151 
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

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

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

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

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

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

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

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

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

1161 

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

1162 
(*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

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

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

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

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

1167 

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

1169 
else warning "The current working directory seems to be no \ 
1408  1170 
\subdirectory of\nIsabelle's main directory. \ 
1171 
\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

1172 

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

1173 
writeln ("Setting path for index.html to " ^ quote cwd ^ 
1291  1174 
"\nGIF path has been set to " ^ quote (!gif_path)); 
1175 

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

1176 
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

1177 
else () 
1291  1178 
end; 
1179 

1313  1180 
(*Generate index.html*) 
1368  1181 
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

1182 
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

1183 
val theory_list = open_in tlist_path; 
1291  1184 
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

1185 
val dummy = (close_in theory_list; delete_file tlist_path); 
1291  1186 

1313  1187 
val gif_path = relative_path (!index_path) (!gif_path); 
1291  1188 

1189 
(*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

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

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

1192 
val (name, path) = take_prefix (not_equal " ") (explode t); 
1291  1193 

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

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

1195 
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

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

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

1198 
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

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

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

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

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

1203 
end; 
1291  1204 

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

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

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

1209 
then take the last directory of index_path*) 

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

1211 
val subdir = 

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

1213 
else last_elem (space_explode "/" (!index_path)); 

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

1214 
val subdirs = space_explode "/" subdir; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1215 

1408  1216 
(*Look for index.html in superdirectories; stop when Isabelle's 
1217 
main directory is reached*) 

1378  1218 
fun find_super_index [] n = ("", n) 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1219 
 find_super_index (p::ps) n = 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1220 
let val index_path = "/" ^ space_implode "/" (rev ps); 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1221 
in if file_exists (index_path ^ "/index.html") then (index_path, n) 
1408  1222 
else if length subdirs  n >= 0 then find_super_index ps (n+1) 
1223 
else ("", n) 

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

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

1225 
val (super_index, level_diff) = 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1226 
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

1227 
val level = length subdirs  level_diff; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1228 

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

1229 
(*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

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

1231 
let val old_index = open_in (super_index ^ "/index.html"); 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1232 
val content = rev (explode (input (old_index, 999999))); 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1233 
val dummy = close_in old_index; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1234 

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

1235 
val out = open_append (super_index ^ "/index.html"); 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1236 
val rel_path = space_implode "/" (drop (level, subdirs)); 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

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

1238 
output (out, 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1239 
(if nth_elem (3, content) <> "!" then "" 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1240 
else "\n<HR><H3>Subdirectories:</H3>\n") ^ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1241 
"<H3><A HREF = \"" ^ rel_path ^ "/index.html\">" ^ rel_path ^ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1242 
"</A></H3>\n"); 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

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

1244 
end; 
1408  1245 

1246 
(*If index_path is no subdirectory of base_path then the title should 

1247 
not contain the string "Isabelle/"*) 

1248 
val title = (if inside_isabelle then "Isabelle/" else "") ^ subdir; 

1291  1249 
in output (out, 
1408  1250 
"<HTML><HEAD><TITLE>" ^ title ^ "</TITLE></HEAD>\n\ 
1251 
\<BODY><H2>" ^ title ^ "</H2>\n\ 

1291  1252 
\The name of every theory is linked to its theory file<BR>\n\ 
1253 
\<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\ 

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

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

1378  1256 
\\" ALT = /\\></A> stands for supertheories (parent theories)" ^ 
1257 
(if super_index = "" then "" else 

1258 
("<P>\n<A HREF = \"" ^ relative_path (!index_path) super_index ^ 

1259 
"/index.html\">Back</A> to the index of " ^ 

1408  1260 
(if not inside_isabelle then 
1261 
hd (tl (rev (space_explode "/" (!index_path)))) 

1262 
else if level = 0 then "Isabelle logics" 

1378  1263 
else space_implode "/" (take (level, subdirs))))) ^ 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1264 
"\n" ^ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1265 
(if file_exists (tack_on (!index_path) "README.html") then 
1332  1266 
"<BR>View the <A HREF = \"README.html\">ReadMe</A> file.\n" 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1267 
else if file_exists (tack_on (!index_path) "README") then 
1332  1268 
"<BR>View the <A HREF = \"README\">ReadMe</A> file.\n" 
1269 
else "") ^ 

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

1270 
"<HR>" ^ implode (map main_entry theories) ^ "<!>"); 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1271 
close_out out; 
1408  1272 
if super_index = "" orelse (inside_isabelle andalso level = 0) then () 
1273 
else link_directory () 

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

1275 

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

1276 
(*Append section heading to HTML file*) 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1277 
fun section s = 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1278 
case !cur_htmlfile of 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1279 
Some out => (mk_theorems_title out; 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1280 
output (out, "<H3>" ^ s ^ "</H3>\n")) 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1281 
 None => (); 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1282 

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