author  wenzelm 
Mon, 29 Jun 1998 10:32:06 +0200  
changeset 5090  75ac9b451ae0 
parent 5038  301c37df931d 
child 5209  a69fe5a61b6c 
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 

3602  7 
Functions for reading theory files. 
391  8 
*) 
9 

3619  10 
signature THY_READ = 
391  11 
sig 
12 
datatype basetype = Thy of string 

13 
 File of string 

14 

15 
val loadpath : string list ref 

16 
val delete_tmpfiles: bool ref 

17 

18 
val use_thy : string > unit 

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

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

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

21 
val exit_use_dir : string > unit 
391  22 
val update : unit > unit 
23 
val unlink_thy : string > unit 

3876  24 
val mk_base : basetype list > string > theory 
391  25 
end; 
26 

27 

3619  28 
structure ThyRead: THY_READ = 
391  29 
struct 
1242  30 

3626  31 
open ThmDatabase ThyInfo BrowserInfo; 
3602  32 

391  33 

34 
datatype basetype = Thy of string 

35 
 File of string; 

36 

3602  37 

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

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

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

40 

3602  41 

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

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

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

44 
val tmp_loadpath = ref [] : string list ref; 
1291  45 

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

46 

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

47 
(*Remove temporary files after use*) 
3602  48 
val delete_tmpfiles = ref true; 
49 

391  50 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

51 
(*Make name of the TextIO.output ML file for a theory *) 
4429  52 
fun out_name tname = File.tmp_name (tname ^ "_thy.ML"); 
391  53 

3602  54 

3626  55 
(*Read a file specified by thy_file containing theory tname*) 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

56 
fun read_thy tname thy_file = 
559  57 
let 
4218  58 
val intext = File.read thy_file; 
3619  59 
val outext = ThySyn.parse tname intext; 
3626  60 
in 
4218  61 
File.write (out_name tname) outext 
3626  62 
end; 
391  63 

64 

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

65 
(*Check if a theory was completly loaded *) 
391  66 
fun already_loaded thy = 
67 
let val t = get_thyinfo thy 

68 
in if is_none t then false 

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

70 
in is_some thy_time andalso is_some ml_time end 
391  71 
end; 
72 

3602  73 

391  74 
(*Check if a theory file has changed since its last use. 
75 
Return a pair of boolean values for .thy and for .ML *) 

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

77 
case get_thyinfo thy of 
3976  78 
Some {thy_time, ml_time, ...} => 
1098
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

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

80 
val mn = is_none ml_time 
391  81 
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

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

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

84 
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

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

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

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

89 
 None => (false, false) 
391  90 

1242  91 

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

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

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

94 
 get_descendants (t :: ts) = 
1291  95 
let val children = children_of t 
96 
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

97 

1291  98 

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

101 
fun find_file "" name = 

1291  102 
let fun find_it (cur :: paths) = 
4218  103 
if File.exists (tack_on cur name) then 
1291  104 
(if cur = "." then name else tack_on cur name) 
559  105 
else 
1291  106 
find_it paths 
391  107 
 find_it [] = "" 
1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

108 
in find_it (!tmp_loadpath @ !loadpath) end 
391  109 
 find_file path name = 
4218  110 
if File.exists (tack_on path name) then tack_on path name 
391  111 
else ""; 
112 

3602  113 

391  114 
(*Get absolute pathnames for a new or already loaded theory *) 
115 
fun get_filenames path name = 

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

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

117 
let val found = find_file path (name ^ ".thy"); 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

118 
val absolute_path = absolute_path (OS.FileSys.getDir ()); 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

119 
val thy_file = absolute_path found; 
391  120 
val (thy_path, _) = split_filename thy_file; 
121 
val found = find_file path (name ^ ".ML"); 

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

122 
val ml_file = if thy_file = "" then absolute_path found 
4218  123 
else if File.exists (tack_on thy_path (name ^ ".ML")) 
391  124 
then tack_on thy_path (name ^ ".ML") 
125 
else ""; 

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

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

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

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

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

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

133 
else (); 

559  134 
(thy_file, ml_file) 
391  135 
end; 
136 

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

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

138 
in if is_some tinfo andalso path = "" then 
3976  139 
let val {path = abs_path, ...} = the tinfo; 
391  140 
val (thy_file, ml_file) = if abs_path = "" then new_filename () 
141 
else (find_file abs_path (name ^ ".thy"), 

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

143 
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

144 
(warning ("File \"" ^ (tack_on path name) 
391  145 
^ ".thy\"\ncontaining theory \"" ^ name 
146 
^ "\" no longer exists."); 

147 
new_filename () 

148 
) 

149 
else (thy_file, ml_file) 

150 
end 

151 
else new_filename () 

152 
end; 

153 

3602  154 

391  155 
(*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

156 
fun unlink_thy tname = 
4111  157 
let fun remove ({path, children, parents, thy_time, ml_time, theory}) = 
3976  158 
{path = path, children = children \ tname, parents = parents, 
4111  159 
thy_time = thy_time, ml_time = ml_time, theory = theory} 
559  160 
in loaded_thys := Symtab.map remove (!loaded_thys) end; 
391  161 

3602  162 

391  163 
(*Remove a theory from loaded_thys *) 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

164 
fun remove_thy tname = 
559  165 
loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname) 
166 
(Symtab.dest (!loaded_thys))); 

391  167 

3602  168 

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

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

170 
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

171 
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of 
4111  172 
Some ({path, children, parents, theory, thy_time = _, ml_time = _}) => 
3976  173 
{path = path, children = children, parents = parents, 
4111  174 
thy_time = thy_time, ml_time = ml_time, theory = theory} 
1291  175 
 None => error ("set_info: theory " ^ tname ^ " not found"); 
1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset

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

3602  178 

391  179 
(*Mark theory as changed since last read if it has been completly read *) 
559  180 
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

181 
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

182 
in if is_none t then () 
1291  183 
else 
3976  184 
let val {thy_time, ml_time, ...} = the t 
1291  185 
in set_info tname (if is_none thy_time then None else Some "") 
186 
(if is_none ml_time then None else Some "") 

187 
end 

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

188 
end; 
391  189 

1656  190 

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

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

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

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

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

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

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

201 
fun use_thy1 tmp_loadpath_valid name = 
1242  202 
let 
203 
val (path, tname) = split_filename name; 

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

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

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

206 
else !tmp_loadpath)); 
1242  207 
val (thy_file, ml_file) = get_filenames path tname; 
208 
val (abs_path, _) = if thy_file = "" then split_filename ml_file 

209 
else split_filename thy_file; 

210 
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

211 
val old_parents = parents_of_name tname; 
391  212 

1242  213 
(*Set absolute path for loaded theory *) 
214 
fun set_path () = 

4111  215 
let val {path = _, children, parents, thy_time, ml_time, theory} = 
1242  216 
the (Symtab.lookup (!loaded_thys, tname)); 
217 
in loaded_thys := Symtab.update ((tname, 

3976  218 
{path = abs_path, 
1291  219 
children = children, parents = parents, 
1242  220 
thy_time = thy_time, ml_time = ml_time, 
4111  221 
theory = theory}), 
1242  222 
!loaded_thys) 
223 
end; 

224 

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

226 
fun mark_children thy = 

1291  227 
let val children = children_of thy; 
1242  228 
val present = filter (is_some o get_thyinfo) children; 
229 
val loaded = filter already_loaded present; 

230 
in if loaded <> [] then 

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

232 
^ " are now outofdate: " 

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

234 
else (); 

235 
seq mark_outdated present 

236 
end; 

391  237 

1554  238 
(*Make sure that loaded_thys contains an entry for tname*) 
239 
fun init_thyinfo () = 

3976  240 
let val tinfo = {path = "", children = [], parents = [], 
1554  241 
thy_time = None, ml_time = None, 
4111  242 
theory = None}; 
1554  243 
in if is_some (get_thyinfo tname) then () 
244 
else loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) 

245 
end; 

1242  246 
in if thy_uptodate andalso ml_uptodate then () 
247 
else 

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

248 
(if thy_file = "" then () 
391  249 
else 
1242  250 
(writeln ("Reading \"" ^ name ^ ".thy\""); 
1291  251 

1554  252 
init_thyinfo (); 
1242  253 
read_thy tname thy_file; 
4218  254 
Use.use (out_name tname); 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

255 

1242  256 
if not (!delete_tmpfiles) then () 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

257 
else OS.FileSys.remove (out_name tname); 
1291  258 

3602  259 
thyfile2html tname abs_path 
1242  260 
); 
1386
cf066d9b4c4f
fixed bug: cur_thyname was overwritten because of early assignment
clasohm
parents:
1378
diff
changeset

261 

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

262 
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

263 
(*mark thy_file as successfully loaded*) 
391  264 

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

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

268 

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

269 
(*Store theory again because it could have been redefined*) 
5090  270 
use_text false ("val _ = store_theory " ^ tname ^ ".thy;"); 
391  271 

1313  272 
(*Add theory to list of all loaded theories (for index.html) 
1291  273 
and add it to its parents' subcharts*) 
3602  274 
let val path = path_of tname; 
275 
in if path = "" then (*first time theory has been read*) 

276 
( 

277 
(*Add theory to list of all loaded theories (for index.html) 

278 
and add it to its parents' subcharts*) 

279 
mk_html tname abs_path old_parents; 

280 

281 
(*Add theory to graph definition file*) 

282 
mk_graph tname abs_path 

283 
) 

284 
else () 

285 
end; 

1291  286 

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

288 
set_info tname (Some (file_info thy_file)) (Some (file_info ml_file)); 
1242  289 
set_path (); 
290 

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

1291  292 
mark_children tname; 
293 

294 
(*Close HTML file*) 

3602  295 
close_html () 
1242  296 
) 
297 
end; 

391  298 

3602  299 

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

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

301 

3602  302 

391  303 
fun time_use_thy tname = timeit(fn()=> 
559  304 
(writeln("\n**** Starting Theory " ^ tname ^ " ****"); 
391  305 
use_thy tname; 
306 
writeln("\n**** Finished Theory " ^ tname ^ " ****")) 

307 
); 

308 

3602  309 

391  310 
(*Load all thy or ML files that have been changed and also 
1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

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

313 
let (*List theories in the order they have to be loaded in.*) 
391  314 
fun load_order [] result = result 
315 
 load_order thys result = 

1291  316 
let fun next_level [] = [] 
317 
 next_level (t :: ts) = 

318 
let val children = children_of t 

319 
in children union (next_level ts) end; 

559  320 

1291  321 
val descendants = next_level thys; 
322 
in load_order descendants ((result \\ descendants) @ descendants) 

323 
end; 

391  324 

325 
fun reload_changed (t :: ts) = 

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

326 
let val abspath = case get_thyinfo t of 
3976  327 
Some ({path, ...}) => path 
1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

328 
 None => ""; 
391  329 

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

330 
val (thy_file, ml_file) = get_filenames abspath t; 
391  331 
val (thy_uptodate, ml_uptodate) = 
332 
thy_unchanged t thy_file ml_file; 

333 
in if thy_uptodate andalso ml_uptodate then () 

334 
else use_thy t; 

335 
reload_changed ts 

336 
end 

337 
 reload_changed [] = (); 

338 

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

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

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

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

344 
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

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

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

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

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

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

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

353 
reload_changed (load_order ["Pure", "CPure"] []) 
391  354 
end; 
355 

3602  356 

391  357 
(*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

358 
Base members are only loaded if they are missing.*) 
3876  359 
fun mk_base bases child = 
1291  360 
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

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

362 
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

363 
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

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

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

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

367 
else if is_some tinfo then 
3976  368 
let val {children, ...} = the tinfo 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

369 
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

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

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

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

373 
in find_it "" child end; 
391  374 

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

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

377 
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

378 
else (); 
559  379 

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

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

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

383 
case Symtab.lookup (!loaded_thys, base) of 
3976  384 
Some ({path, children, parents, thy_time, ml_time, 
4111  385 
theory}) => 
3976  386 
{path = path, 
1291  387 
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

388 
thy_time = thy_time, ml_time = ml_time, 
4111  389 
theory = theory} 
3976  390 
 None => {path = "", children = [child], parents = [], 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

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

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

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

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

396 
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

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

398 
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

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

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

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

402 
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

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

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

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

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

407 
if thy_loaded then () 
3876  408 
else (writeln ("Autoloading theory " ^ quote base 
409 
^ " (required by " ^ quote child ^ ")"); 

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

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

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

412 
end; 
391  413 

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

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

415 
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

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

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

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

420 
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

421 
 load_base [] = []; 
391  422 

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

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

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

425 

3876  426 
val base_thy = 
427 
(writeln ("Loading theory " ^ quote child); 

3998  428 
if null mergelist then ProtoPure.thy 
429 
else Theory.prep_ext_merge (map theory_of mergelist)); 

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

430 

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

4111  433 
Some ({path, children, parents = _, thy_time, ml_time, theory}) => 
434 
{path = path, children = children, parents = mergelist, 

435 
thy_time = thy_time, ml_time = ml_time, theory = theory} 

436 
 None => sys_error ("set_parents: theory " ^ child ^ " not found"); 

1291  437 
in loaded_thys := Symtab.update ((child, tinfo), !loaded_thys) end; 
438 

4111  439 
in 
440 
cur_thyname := child; 

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

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

442 
end; 
391  443 

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

444 

1670
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset

445 
(*Temporarily enter a directory and load its ROOT.ML file; 
3602  446 
also do some work for HTML and graph generation*) 
1670
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset

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

448 

1670
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset

449 
fun gen_use_dir use_cmd dirname = 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

450 
let val old_dir = OS.FileSys.getDir (); 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

451 
in OS.FileSys.chDir dirname; 
1670
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset

452 
if !make_html then init_html() else (); 
3602  453 
if !make_graph then init_graph dirname else (); 
1670
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset

454 
use_cmd "ROOT.ML"; 
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset

455 
finish_html(); 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

456 
OS.FileSys.chDir old_dir 
1670
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset

457 
end; 
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset

458 

d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset

459 
in 
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset

460 

4218  461 
val use_dir = gen_use_dir Use.use; 
462 
val exit_use_dir = gen_use_dir Use.exit_use; 

1670
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset

463 

d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset

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

465 

391  466 
end; 