author | wenzelm |
Fri, 24 Oct 1997 17:18:49 +0200 | |
changeset 3998 | 6ec8d42082f1 |
parent 3976 | 1030dd79720b |
child 4021 | 4e2994bae718 |
permissions | -rw-r--r-- |
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 *) |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
52 |
fun out_name tname = "." ^ 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 |
3626 | 58 |
val intext = read_file thy_file; |
3619 | 59 |
val outext = ThySyn.parse tname intext; |
3626 | 60 |
in |
61 |
write_file (out_name tname) outext |
|
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) = |
103 |
if file_exists (tack_on cur name) then |
|
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 = |
110 |
if file_exists (tack_on path name) then tack_on path name |
|
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 |
391 | 123 |
else if file_exists (tack_on thy_path (name ^ ".ML")) |
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 = |
3976 | 157 |
let fun remove ({path, children, parents, thy_time, ml_time, |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
158 |
theory, thms, methods, data}) = |
3976 | 159 |
{path = path, children = children \ tname, parents = parents, |
1242 | 160 |
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
|
161 |
thms = thms, methods = methods, data = data} |
559 | 162 |
in loaded_thys := Symtab.map remove (!loaded_thys) end; |
391 | 163 |
|
3602 | 164 |
|
391 | 165 |
(*Remove a theory from loaded_thys *) |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
166 |
fun remove_thy tname = |
559 | 167 |
loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname) |
168 |
(Symtab.dest (!loaded_thys))); |
|
391 | 169 |
|
3602 | 170 |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
171 |
(*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
|
172 |
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
|
173 |
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of |
3976 | 174 |
Some ({path, children, parents, theory, thms, |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
175 |
methods, data, ...}) => |
3976 | 176 |
{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
|
177 |
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
|
178 |
theory = theory, thms = thms, |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
179 |
methods = methods, data = data} |
1291 | 180 |
| None => error ("set_info: theory " ^ tname ^ " not found"); |
1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
181 |
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; |
391 | 182 |
|
3602 | 183 |
|
391 | 184 |
(*Mark theory as changed since last read if it has been completly read *) |
559 | 185 |
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
|
186 |
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
|
187 |
in if is_none t then () |
1291 | 188 |
else |
3976 | 189 |
let val {thy_time, ml_time, ...} = the t |
1291 | 190 |
in set_info tname (if is_none thy_time then None else Some "") |
191 |
(if is_none ml_time then None else Some "") |
|
192 |
end |
|
971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
193 |
end; |
391 | 194 |
|
1656 | 195 |
|
559 | 196 |
(*Read .thy and .ML files that haven't been read yet or have changed since |
391 | 197 |
they were last read; |
559 | 198 |
loaded_thys is a thy_info list ref containing all theories that have |
391 | 199 |
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
|
200 |
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
|
201 |
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
|
202 |
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
|
203 |
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
|
204 |
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
|
205 |
*) |
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset
|
206 |
fun use_thy1 tmp_loadpath_valid name = |
1242 | 207 |
let |
208 |
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
|
209 |
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
|
210 |
(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
|
211 |
else !tmp_loadpath)); |
1242 | 212 |
val (thy_file, ml_file) = get_filenames path tname; |
213 |
val (abs_path, _) = if thy_file = "" then split_filename ml_file |
|
214 |
else split_filename thy_file; |
|
215 |
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
|
216 |
val old_parents = parents_of_name tname; |
391 | 217 |
|
1242 | 218 |
(*Set absolute path for loaded theory *) |
219 |
fun set_path () = |
|
3976 | 220 |
let val {children, parents, thy_time, ml_time, theory, thms, |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
221 |
methods, data, ...} = |
1242 | 222 |
the (Symtab.lookup (!loaded_thys, tname)); |
223 |
in loaded_thys := Symtab.update ((tname, |
|
3976 | 224 |
{path = abs_path, |
1291 | 225 |
children = children, parents = parents, |
1242 | 226 |
thy_time = thy_time, ml_time = ml_time, |
227 |
theory = theory, thms = thms, |
|
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
228 |
methods = methods, data = data}), |
1242 | 229 |
!loaded_thys) |
230 |
end; |
|
231 |
||
232 |
(*Mark all direct descendants of a theory as changed *) |
|
233 |
fun mark_children thy = |
|
1291 | 234 |
let val children = children_of thy; |
1242 | 235 |
val present = filter (is_some o get_thyinfo) children; |
236 |
val loaded = filter already_loaded present; |
|
237 |
in if loaded <> [] then |
|
238 |
writeln ("The following children of theory " ^ (quote thy) |
|
239 |
^ " are now out-of-date: " |
|
240 |
^ (quote (space_implode "\",\"" loaded))) |
|
241 |
else (); |
|
242 |
seq mark_outdated present |
|
243 |
end; |
|
391 | 244 |
|
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
245 |
(*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
|
246 |
data table*) |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
247 |
fun save_data thy_only = |
3976 | 248 |
let val {path, children, parents, thy_time, ml_time, |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
249 |
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
|
250 |
|
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
251 |
fun get_data [] data = data |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
252 |
| get_data ((id, ThyMethods {get, ...}) :: ms) data = |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
253 |
get_data ms (Symtab.update ((id, get ()), data)); |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
254 |
|
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
255 |
val new_data = get_data (Symtab.dest methods) Symtab.null; |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
256 |
|
3039
bbf4e3738ef0
get_thydata accesses the second component of the data field. This component
nipkow
parents:
2406
diff
changeset
|
257 |
val data' = (if thy_only then new_data else fst data, new_data) |
bbf4e3738ef0
get_thydata accesses the second component of the data field. This component
nipkow
parents:
2406
diff
changeset
|
258 |
(* 2nd component must be up to date *) |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
259 |
in loaded_thys := Symtab.update |
3976 | 260 |
((tname, {path = path, |
1291 | 261 |
children = children, parents = parents, |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
262 |
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
|
263 |
theory = theory, thms = thms, |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
264 |
methods = methods, data = data'}), |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
265 |
!loaded_thys) |
1242 | 266 |
end; |
267 |
||
1554 | 268 |
(*Make sure that loaded_thys contains an entry for tname*) |
269 |
fun init_thyinfo () = |
|
3976 | 270 |
let val tinfo = {path = "", children = [], parents = [], |
1554 | 271 |
thy_time = None, ml_time = None, |
272 |
theory = None, thms = Symtab.null, |
|
273 |
methods = Symtab.null, |
|
274 |
data = (Symtab.null, Symtab.null)}; |
|
275 |
in if is_some (get_thyinfo tname) then () |
|
276 |
else loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) |
|
277 |
end; |
|
1242 | 278 |
in if thy_uptodate andalso ml_uptodate then () |
279 |
else |
|
1386
cf066d9b4c4f
fixed bug: cur_thyname was overwritten because of early assignment
clasohm
parents:
1378
diff
changeset
|
280 |
(if thy_file = "" then () |
1656 | 281 |
else if thy_uptodate then put_thydata true tname |
391 | 282 |
else |
1242 | 283 |
(writeln ("Reading \"" ^ name ^ ".thy\""); |
1291 | 284 |
|
1554 | 285 |
init_thyinfo (); |
1530 | 286 |
delete_thms tname; |
1242 | 287 |
read_thy tname thy_file; |
2406 | 288 |
SymbolInput.use (out_name tname); |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
289 |
save_data true; |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
290 |
|
1308 | 291 |
(*Store axioms of theory |
292 |
(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
|
293 |
let val parents = parents_of_name tname; |
1308 | 294 |
val this_thy = theory_of tname; |
295 |
val axioms = |
|
296 |
if length parents = 1 |
|
297 |
andalso Sign.eq_sg (sign_of (theory_of (hd parents)), |
|
298 |
sign_of this_thy) then [] |
|
299 |
else axioms_of this_thy; |
|
300 |
in map store_thm_db axioms end; |
|
301 |
||
1242 | 302 |
if not (!delete_tmpfiles) then () |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset
|
303 |
else OS.FileSys.remove (out_name tname); |
1291 | 304 |
|
3602 | 305 |
thyfile2html tname abs_path |
1242 | 306 |
); |
1386
cf066d9b4c4f
fixed bug: cur_thyname was overwritten because of early assignment
clasohm
parents:
1378
diff
changeset
|
307 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
308 |
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
|
309 |
(*mark thy_file as successfully loaded*) |
391 | 310 |
|
1242 | 311 |
if ml_file = "" then () |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
312 |
else (writeln ("Reading \"" ^ name ^ ".ML\""); |
2406 | 313 |
SymbolInput.use ml_file); |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
314 |
save_data false; |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
315 |
|
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
316 |
(*Store theory again because it could have been redefined*) |
3631 | 317 |
use_strings |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
318 |
["val _ = store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"]; |
391 | 319 |
|
1313 | 320 |
(*Add theory to list of all loaded theories (for index.html) |
1291 | 321 |
and add it to its parents' sub-charts*) |
3602 | 322 |
let val path = path_of tname; |
323 |
in if path = "" then (*first time theory has been read*) |
|
324 |
( |
|
325 |
(*Add theory to list of all loaded theories (for index.html) |
|
326 |
and add it to its parents' sub-charts*) |
|
327 |
mk_html tname abs_path old_parents; |
|
328 |
||
329 |
(*Add theory to graph definition file*) |
|
330 |
mk_graph tname abs_path |
|
331 |
) |
|
332 |
else () |
|
333 |
end; |
|
1291 | 334 |
|
1242 | 335 |
(*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
|
336 |
set_info tname (Some (file_info thy_file)) (Some (file_info ml_file)); |
1242 | 337 |
set_path (); |
338 |
||
339 |
(*Mark theories that have to be reloaded*) |
|
1291 | 340 |
mark_children tname; |
341 |
||
342 |
(*Close HTML file*) |
|
3602 | 343 |
close_html () |
1242 | 344 |
) |
345 |
end; |
|
391 | 346 |
|
3602 | 347 |
|
1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset
|
348 |
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
|
349 |
|
3602 | 350 |
|
391 | 351 |
fun time_use_thy tname = timeit(fn()=> |
559 | 352 |
(writeln("\n**** Starting Theory " ^ tname ^ " ****"); |
391 | 353 |
use_thy tname; |
354 |
writeln("\n**** Finished Theory " ^ tname ^ " ****")) |
|
355 |
); |
|
356 |
||
3602 | 357 |
|
391 | 358 |
(*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
|
359 |
all theories that depend on them.*) |
391 | 360 |
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
|
361 |
let (*List theories in the order they have to be loaded in.*) |
391 | 362 |
fun load_order [] result = result |
363 |
| load_order thys result = |
|
1291 | 364 |
let fun next_level [] = [] |
365 |
| next_level (t :: ts) = |
|
366 |
let val children = children_of t |
|
367 |
in children union (next_level ts) end; |
|
559 | 368 |
|
1291 | 369 |
val descendants = next_level thys; |
370 |
in load_order descendants ((result \\ descendants) @ descendants) |
|
371 |
end; |
|
391 | 372 |
|
373 |
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
|
374 |
let val abspath = case get_thyinfo t of |
3976 | 375 |
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
|
376 |
| None => ""; |
391 | 377 |
|
1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset
|
378 |
val (thy_file, ml_file) = get_filenames abspath t; |
391 | 379 |
val (thy_uptodate, ml_uptodate) = |
380 |
thy_unchanged t thy_file ml_file; |
|
381 |
in if thy_uptodate andalso ml_uptodate then () |
|
382 |
else use_thy t; |
|
383 |
reload_changed ts |
|
384 |
end |
|
385 |
| reload_changed [] = (); |
|
386 |
||
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
387 |
(*Remove all theories that are no descendants of ProtoPure. |
391 | 388 |
If there are still children in the deleted theory's list |
389 |
schedule them for reloading *) |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
390 |
fun collect_garbage no_garbage = |
3976 | 391 |
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
|
392 |
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
|
393 |
else (writeln ("Theory \"" ^ tname ^ |
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
394 |
"\" is no longer linked with ProtoPure - removing it."); |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
395 |
remove_thy tname; |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
396 |
seq mark_outdated children) |
391 | 397 |
| collect [] = () |
559 | 398 |
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
|
399 |
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
|
400 |
collect_garbage ("ProtoPure" :: (load_order ["ProtoPure"] [])); |
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
401 |
reload_changed (load_order ["Pure", "CPure"] []) |
391 | 402 |
end; |
403 |
||
3602 | 404 |
|
391 | 405 |
(*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
|
406 |
Base members are only loaded if they are missing.*) |
3876 | 407 |
fun mk_base bases child = |
1291 | 408 |
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
|
409 |
fun show_cycle base = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
410 |
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
|
411 |
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
|
412 |
in if base = curr then |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
413 |
error ("Cyclic dependency of theories: " |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
414 |
^ child ^ "->" ^ base ^ result) |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
415 |
else if is_some tinfo then |
3976 | 416 |
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
|
417 |
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
|
418 |
end |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
419 |
else () |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
420 |
end |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
421 |
in find_it "" child end; |
391 | 422 |
|
1291 | 423 |
(*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
|
424 |
fun find_cycle base = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
425 |
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
|
426 |
else (); |
559 | 427 |
|
1291 | 428 |
(*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
|
429 |
fun add_child base = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
430 |
let val tinfo = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
431 |
case Symtab.lookup (!loaded_thys, base) of |
3976 | 432 |
Some ({path, children, parents, thy_time, ml_time, |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
433 |
theory, thms, methods, data}) => |
3976 | 434 |
{path = path, |
1291 | 435 |
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
|
436 |
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
|
437 |
theory = theory, thms = thms, |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
438 |
methods = methods, data = data} |
3976 | 439 |
| 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
|
440 |
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
|
441 |
theory = None, thms = Symtab.null, |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
442 |
methods = Symtab.null, |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
443 |
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
|
444 |
in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end; |
559 | 445 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
446 |
(*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
|
447 |
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
|
448 |
fun load base = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
449 |
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
|
450 |
(*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
|
451 |
in |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
452 |
if child = base then |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
453 |
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
|
454 |
^ "->" ^ child) |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
455 |
else |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
456 |
(find_cycle base; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
457 |
add_child base; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
458 |
if thy_loaded then () |
3876 | 459 |
else (writeln ("Autoloading theory " ^ quote base |
460 |
^ " (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
|
461 |
use_thy1 true base) |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
462 |
) |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
463 |
end; |
391 | 464 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
465 |
(*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
|
466 |
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
|
467 |
(load b; |
1291 | 468 |
b :: load_base bs) |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
469 |
| load_base (File b :: bs) = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
470 |
(load b; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
471 |
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
|
472 |
| load_base [] = []; |
391 | 473 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
474 |
val dummy = unlink_thy child; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
475 |
val mergelist = load_base bases; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
476 |
|
3876 | 477 |
val base_thy = |
478 |
(writeln ("Loading theory " ^ quote child); |
|
3998 | 479 |
if null mergelist then ProtoPure.thy |
480 |
else Theory.prep_ext_merge (map theory_of mergelist)); |
|
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
481 |
|
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
482 |
val datas = |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
483 |
let fun get_data t = |
3976 | 484 |
let val {data, ...} = the (get_thyinfo t) |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
485 |
in snd data end; |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
486 |
in map (Symtab.dest o get_data) mergelist end; |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
487 |
|
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
488 |
val methods = |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
489 |
let fun get_methods t = |
3976 | 490 |
let val {methods, ...} = the (get_thyinfo t) |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
491 |
in methods end; |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
492 |
|
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
493 |
val ms = map get_methods mergelist; |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
494 |
in if null ms then Symtab.null |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
495 |
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
|
496 |
end; |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
497 |
|
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
498 |
(*merge two sorted association lists*) |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
499 |
fun merge_two ([], d2) = d2 |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
500 |
| merge_two (d1, []) = d1 |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
501 |
| merge_two (l1 as ((p1 as (id1 : string, d1)) :: d1s), |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
502 |
l2 as ((p2 as (id2, d2)) :: d2s)) = |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
503 |
if id1 < id2 then |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
504 |
p1 :: merge_two (d1s, l2) |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
505 |
else |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
506 |
p2 :: merge_two (l1, d2s); |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
507 |
|
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
508 |
(*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
|
509 |
fun merge_multi [] None = [] |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
510 |
| merge_multi [] (Some (id, ds)) = |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
511 |
let val ThyMethods {merge, put, ...} = |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
512 |
the (Symtab.lookup (methods, id)); |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
513 |
in put (merge ds); [id] end |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
514 |
| 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
|
515 |
| merge_multi ((id, d) :: ds) (Some (id2, d2s)) = |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
516 |
if id = id2 then |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
517 |
merge_multi ds (Some (id2, d :: d2s)) |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
518 |
else |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
519 |
let val ThyMethods {merge, put, ...} = |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
520 |
the (Symtab.lookup (methods, id2)); |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
521 |
in put (merge d2s); |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
522 |
id2 :: merge_multi ds (Some (id, [d])) |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
523 |
end; |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
524 |
|
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
525 |
val merged = |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
526 |
if null datas then [] |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
527 |
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
|
528 |
|
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
529 |
val dummy = |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
530 |
let val unmerged = map fst (Symtab.dest methods) \\ merged; |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
531 |
|
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
532 |
fun put_empty id = |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
533 |
let val ThyMethods {merge, put, ...} = |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
534 |
the (Symtab.lookup (methods, id)); |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
535 |
in put (merge []) end; |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
536 |
in seq put_empty unmerged end; |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
537 |
|
1291 | 538 |
val dummy = |
539 |
let val tinfo = case Symtab.lookup (!loaded_thys, child) of |
|
3976 | 540 |
Some ({path, children, thy_time, ml_time, theory, thms, |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
541 |
data, ...}) => |
3976 | 542 |
{path = path, |
1291 | 543 |
children = children, parents = mergelist, |
544 |
thy_time = thy_time, ml_time = ml_time, |
|
545 |
theory = theory, thms = thms, |
|
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
546 |
methods = methods, data = data} |
1291 | 547 |
| None => error ("set_parents: theory " ^ child ^ " not found"); |
548 |
in loaded_thys := Symtab.update ((child, tinfo), !loaded_thys) end; |
|
549 |
||
1386
cf066d9b4c4f
fixed bug: cur_thyname was overwritten because of early assignment
clasohm
parents:
1378
diff
changeset
|
550 |
in cur_thyname := child; |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
551 |
base_thy |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
552 |
end; |
391 | 553 |
|
1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
554 |
|
1670
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
555 |
(*Temporarily enter a directory and load its ROOT.ML file; |
3602 | 556 |
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
|
557 |
local |
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
558 |
|
1670
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
559 |
fun gen_use_dir use_cmd dirname = |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset
|
560 |
let val old_dir = OS.FileSys.getDir (); |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset
|
561 |
in OS.FileSys.chDir dirname; |
1670
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
562 |
if !make_html then init_html() else (); |
3602 | 563 |
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
|
564 |
use_cmd "ROOT.ML"; |
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
565 |
finish_html(); |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset
|
566 |
OS.FileSys.chDir old_dir |
1670
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
567 |
end; |
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
568 |
|
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
569 |
in |
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
570 |
|
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
571 |
val use_dir = gen_use_dir use; |
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
572 |
val exit_use_dir = gen_use_dir exit_use; |
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
573 |
|
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
574 |
end |
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
575 |
|
391 | 576 |
end; |