--- a/src/Pure/Thy/thy_info.ML Wed Feb 03 20:25:01 1999 +0100
+++ b/src/Pure/Thy/thy_info.ML Wed Feb 03 20:25:53 1999 +0100
@@ -6,9 +6,7 @@
and user data.
TODO:
- - check_thy: include ML stamp (!?!?);
- check all these versions of 'use' (!!);
- - errors during require etc.: include initiators (!?);
- data: ThyInfoFun;
- remove operation (GC!?);
- update_all operation (!?);
@@ -240,7 +238,7 @@
| Some {present, outdated, master, files} =>
if present andalso not strict then (true, same_deps)
else
- let val master' = Some (ThyLoad.check_thy name) in
+ let val master' = Some (ThyLoad.check_thy name ml) in
if master <> master' then (false, load_deps name ml)
else (not outdated andalso forall file_current files, same_deps)
end)
@@ -249,6 +247,10 @@
fun outdated name =
(case lookup_deps name of Some (Some {outdated, ...}) => outdated | _ => false);
+fun untouch None = None
+ | untouch (Some {present, outdated = _, master, files}) =
+ make_depends present false master files;
+
fun require_thy ml time strict keep_strict initiators name =
let
val require_parent =
@@ -262,7 +264,7 @@
if current andalso pre_outdated = outdated name then () (* FIXME ?? *)
else
((case new_deps of
- Some deps => change_thys (update_node name parents (deps, None))
+ Some deps => change_thys (update_node name parents (untouch deps, None))
| None => ()); load_thy ml time initiators name parents)
end;