243 if master <> master' then (false, load_deps dir name ml) |
243 if master <> master' then (false, load_deps dir name ml) |
244 else (not outdated andalso forall file_current files, same_deps) |
244 else (not outdated andalso forall file_current files, same_deps) |
245 end) |
245 end) |
246 end); |
246 end); |
247 |
247 |
248 fun require_thy ml time strict keep_strict initiators prfx s = |
248 fun require_thy ml time strict keep_strict initiators prfx (visited, str) = |
249 let |
249 let |
250 val path = Path.expand (Path.unpack s); |
250 val path = Path.expand (Path.unpack str); |
251 val name = Path.pack (Path.base path); |
251 val name = Path.pack (Path.base path); |
252 val dir = Path.append prfx (Path.dir path); |
252 in |
253 |
253 if name mem_string visited then (visited, (true, name)) |
254 val require_parent = |
254 else |
255 #1 o require_thy ml time (strict andalso keep_strict) keep_strict (name :: initiators) dir; |
255 let |
256 val (current, (new_deps, parents)) = current_deps ml strict dir name handle ERROR => |
256 val dir = Path.append prfx (Path.dir path); |
257 error (loader_msg "The error(s) above occurred while examining theory" [name] ^ |
257 val req_parent = |
258 (if null initiators then "" else "\n" ^ required_by initiators)); |
258 require_thy ml time (strict andalso keep_strict) keep_strict (name :: initiators) dir; |
259 val parents_current = map require_parent parents; |
259 |
260 |
260 val (current, (new_deps, parents)) = current_deps ml strict dir name handle ERROR => |
261 val result = |
261 error (loader_msg "The error(s) above occurred while examining theory" [name] ^ |
262 if current andalso forall I parents_current then true |
262 (if null initiators then "" else "\n" ^ required_by initiators)); |
263 else |
263 val (visited', parent_results) = foldl_map req_parent (name :: visited, parents); |
264 ((case new_deps of |
264 |
265 Some deps => change_thys (update_node name parents (untouch_deps deps, None)) |
265 val result = |
266 | None => ()); |
266 if current andalso forall #1 parent_results then true |
267 load_thy ml time initiators dir name parents; |
267 else |
268 false); |
268 ((case new_deps of |
269 in (result, name) end; |
269 Some deps => change_thys (update_node name parents (untouch_deps deps, None)) |
270 |
270 | None => ()); |
271 fun gen_use_thy f s = |
271 load_thy ml time initiators dir name parents; |
272 let val (_, name) = f Path.current s in Context.context (get_theory name) end; |
272 false); |
273 |
273 in (visited', (result, name)) end |
274 val weak_use_thy = gen_use_thy (require_thy true false false false []); |
274 end; |
275 val use_thy = gen_use_thy (require_thy true false true false []); |
275 |
276 val update_thy = gen_use_thy (require_thy true false true true []); |
276 fun gen_use_thy req s = |
277 val time_use_thy = gen_use_thy (require_thy true true true false []); |
277 let val (_, (_, name)) = req [] Path.current ([], s) |
278 val use_thy_only = gen_use_thy (require_thy false false true false []); |
278 in Context.context (get_theory name) end; |
|
279 |
|
280 val weak_use_thy = gen_use_thy (require_thy true false false false); |
|
281 val use_thy = gen_use_thy (require_thy true false true false); |
|
282 val update_thy = gen_use_thy (require_thy true false true true); |
|
283 val time_use_thy = gen_use_thy (require_thy true true true false); |
|
284 val use_thy_only = gen_use_thy (require_thy false false true false); |
279 |
285 |
280 |
286 |
281 (* remove_thy *) |
287 (* remove_thy *) |
282 |
288 |
283 fun remove_thy name = |
289 fun remove_thy name = |