author  paulson 
Mon, 05 Oct 1998 10:33:34 +0200  
changeset 5615  9ea709aa275c 
parent 5495  48036910ab7e 
child 5730  82a7aa74a631 
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) 
5495
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

223 
end 
1242  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 

5495
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

236 
end 
391  237 

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

5495
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

240 
let val tinfo = {path = "", children = [], parents = [], 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

241 
thy_time = None, ml_time = None, 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

242 
theory = None}; 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

243 
in if is_some (get_thyinfo tname) then () 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

244 
else loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

245 
end 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

246 
fun read_thy_file() = 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

247 
if thy_file = "" then () 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

248 
else 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

249 
(writeln ("Reading \"" ^ name ^ ".thy\""); 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

250 
init_thyinfo (); 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

251 
read_thy tname thy_file; 
5615
9ea709aa275c
deleted incorrect code that set Goals.proof_timing:=false
paulson
parents:
5495
diff
changeset

252 
Use.use (out_name tname); 
5495
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

253 
if not (!delete_tmpfiles) then () 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

254 
else OS.FileSys.remove (out_name tname); 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

255 
thyfile2html tname abs_path) 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

256 

48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

257 
(*Add theory to list of all loaded theories (for index.html) 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

258 
and it to its parents' subcharts*) 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

259 
fun add_theory path = 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

260 
if path = "" then (*first time theory has been read*) 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

261 
(mk_html tname abs_path old_parents; 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

262 
mk_graph tname abs_path) (*Add it to graph definition file*) 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

263 
else () 
1242  264 
in if thy_uptodate andalso ml_uptodate then () 
265 
else 

5495
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

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

267 
set_info tname (Some (file_info thy_file)) None; 
5495
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

268 
(*mark thy_file as successfully loaded*) 
391  269 

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

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

273 

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

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

5495
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

277 
add_theory (path_of tname); 
1291  278 

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

280 
set_info tname (Some (file_info thy_file)) (Some (file_info ml_file)); 
1242  281 
set_path (); 
5495
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

282 
mark_children tname; (*Mark theories that have to be reloaded*) 
48036910ab7e
Suppress timing messages for theorems proved in theory sections
paulson
parents:
5209
diff
changeset

283 
close_html () ) 
1242  284 
end; 
391  285 

3602  286 

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

287 
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

288 

3602  289 

391  290 
fun time_use_thy tname = timeit(fn()=> 
559  291 
(writeln("\n**** Starting Theory " ^ tname ^ " ****"); 
5615
9ea709aa275c
deleted incorrect code that set Goals.proof_timing:=false
paulson
parents:
5495
diff
changeset

292 
setmp Goals.proof_timing true use_thy tname; 
391  293 
writeln("\n**** Finished Theory " ^ tname ^ " ****")) 
294 
); 

295 

3602  296 

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

298 
all theories that depend on them.*) 
391  299 
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

300 
let (*List theories in the order they have to be loaded in.*) 
391  301 
fun load_order [] result = result 
302 
 load_order thys result = 

1291  303 
let fun next_level [] = [] 
304 
 next_level (t :: ts) = 

305 
let val children = children_of t 

306 
in children union (next_level ts) end; 

559  307 

1291  308 
val descendants = next_level thys; 
309 
in load_order descendants ((result \\ descendants) @ descendants) 

310 
end; 

391  311 

312 
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

313 
let val abspath = case get_thyinfo t of 
3976  314 
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

315 
 None => ""; 
391  316 

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

317 
val (thy_file, ml_file) = get_filenames abspath t; 
391  318 
val (thy_uptodate, ml_uptodate) = 
319 
thy_unchanged t thy_file ml_file; 

320 
in if thy_uptodate andalso ml_uptodate then () 

321 
else use_thy t; 

322 
reload_changed ts 

323 
end 

324 
 reload_changed [] = (); 

325 

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

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

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

329 
fun collect_garbage no_garbage = 
3976  330 
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

331 
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

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

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

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

335 
seq mark_outdated children) 
391  336 
 collect [] = () 
559  337 
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

338 
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

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

340 
reload_changed (load_order ["Pure", "CPure"] []) 
391  341 
end; 
342 

3602  343 

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

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

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

349 
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

350 
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

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

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

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

354 
else if is_some tinfo then 
3976  355 
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

356 
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

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

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

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

360 
in find_it "" child end; 
391  361 

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

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

364 
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

365 
else (); 
559  366 

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

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

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

370 
case Symtab.lookup (!loaded_thys, base) of 
3976  371 
Some ({path, children, parents, thy_time, ml_time, 
4111  372 
theory}) => 
3976  373 
{path = path, 
1291  374 
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

375 
thy_time = thy_time, ml_time = ml_time, 
4111  376 
theory = theory} 
3976  377 
 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

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

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

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

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

383 
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

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

385 
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

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

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

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

389 
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

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

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

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

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

394 
if thy_loaded then () 
3876  395 
else (writeln ("Autoloading theory " ^ quote base 
396 
^ " (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

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

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

399 
end; 
391  400 

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

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

402 
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

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

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

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

407 
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

408 
 load_base [] = []; 
391  409 

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

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

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

412 

3876  413 
val base_thy = 
414 
(writeln ("Loading theory " ^ quote child); 

3998  415 
if null mergelist then ProtoPure.thy 
5209  416 
else Theory.prep_ext_merge (map ThyInfo.theory mergelist)); 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

417 

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

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

422 
thy_time = thy_time, ml_time = ml_time, theory = theory} 

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

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

4111  426 
in 
427 
cur_thyname := child; 

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

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

429 
end; 
391  430 

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

431 

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

432 
(*Temporarily enter a directory and load its ROOT.ML file; 
3602  433 
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

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

435 

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

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

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

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

439 
if !make_html then init_html() else (); 
3602  440 
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

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

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

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

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

445 

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

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

447 

4218  448 
val use_dir = gen_use_dir Use.use; 
449 
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

450 

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

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

452 

391  453 
end; 