src/Pure/Thy/thy_info.ML
changeset 6219 b360065c2b07
parent 6211 43d0efafa025
child 6233 9cc37487f995
     1.1 --- a/src/Pure/Thy/thy_info.ML	Wed Feb 03 20:25:01 1999 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Feb 03 20:25:53 1999 +0100
     1.3 @@ -6,9 +6,7 @@
     1.4  and user data.
     1.5  
     1.6  TODO:
     1.7 -  - check_thy: include ML stamp (!?!?);
     1.8    - check all these versions of 'use' (!!);
     1.9 -  - errors during require etc.: include initiators (!?);
    1.10    - data: ThyInfoFun;
    1.11    - remove operation (GC!?);
    1.12    - update_all operation (!?);
    1.13 @@ -240,7 +238,7 @@
    1.14          | Some {present, outdated, master, files} =>
    1.15              if present andalso not strict then (true, same_deps)
    1.16              else
    1.17 -              let val master' = Some (ThyLoad.check_thy name) in
    1.18 +              let val master' = Some (ThyLoad.check_thy name ml) in
    1.19                  if master <> master' then (false, load_deps name ml)
    1.20                  else (not outdated andalso forall file_current files, same_deps)
    1.21                end)
    1.22 @@ -249,6 +247,10 @@
    1.23  fun outdated name =
    1.24    (case lookup_deps name of Some (Some {outdated, ...}) => outdated | _ => false);
    1.25  
    1.26 +fun untouch None = None
    1.27 +  | untouch (Some {present, outdated = _, master, files}) =
    1.28 +      make_depends present false master files;
    1.29 +
    1.30  fun require_thy ml time strict keep_strict initiators name =
    1.31    let
    1.32      val require_parent =
    1.33 @@ -262,7 +264,7 @@
    1.34      if current andalso pre_outdated = outdated name then ()	(* FIXME ?? *)
    1.35      else
    1.36        ((case new_deps of
    1.37 -        Some deps => change_thys (update_node name parents (deps, None))
    1.38 +        Some deps => change_thys (update_node name parents (untouch deps, None))
    1.39        | None => ()); load_thy ml time initiators name parents)
    1.40    end;
    1.41