check_thy: include ML stamp;
authorwenzelm
Wed Feb 03 20:25:53 1999 +0100 (1999-02-03)
changeset 6219b360065c2b07
parent 6218 3e9d6edc99a8
child 6220 5a29b53eca45
check_thy: include ML stamp;
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
     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  
     2.1 --- a/src/Pure/Thy/thy_load.ML	Wed Feb 03 20:25:01 1999 +0100
     2.2 +++ b/src/Pure/Thy/thy_load.ML	Wed Feb 03 20:25:53 1999 +0100
     2.3 @@ -20,7 +20,7 @@
     2.4    val find_file: Path.T -> (Path.T * File.info) option
     2.5    val check_file: Path.T -> File.info option
     2.6    val load_file: Path.T -> File.info
     2.7 -  val check_thy: string -> File.info
     2.8 +  val check_thy: string -> bool -> File.info
     2.9    val deps_thy: string -> bool -> File.info * (string list * Path.T list)
    2.10    val load_thy: string -> bool -> bool -> File.info
    2.11  end;
    2.12 @@ -86,7 +86,13 @@
    2.13  val deps_thy_fn = ref (undefined: string -> bool -> Path.T -> string list * Path.T list);
    2.14  val load_thy_fn = ref (undefined: string -> bool -> bool -> Path.T -> unit);
    2.15  
    2.16 -val check_thy = #1 o process_thy (K ());
    2.17 +fun check_thy name ml =
    2.18 +  let val (thy_info, _) = process_thy (K ()) name in
    2.19 +    (case if ml then check_file (ml_path name) else None of
    2.20 +      None => thy_info
    2.21 +    | Some info => File.join_info thy_info info)
    2.22 +  end;
    2.23 +
    2.24  fun deps_thy name ml = process_thy (fn path => ! deps_thy_fn name ml path) name;
    2.25  fun load_thy name ml time = #1 (process_thy (fn path => ! load_thy_fn name ml time path) name);
    2.26