# HG changeset patch
# User wenzelm
# Date 918069953 -3600
# Node ID b360065c2b079445e514be35a2169729fed2539b
# Parent  3e9d6edc99a8d321ba9063fbf1897aaabb006363
check_thy: include ML stamp;

diff -r 3e9d6edc99a8 -r b360065c2b07 src/Pure/Thy/thy_info.ML
--- 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;
 
diff -r 3e9d6edc99a8 -r b360065c2b07 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed Feb 03 20:25:01 1999 +0100
+++ b/src/Pure/Thy/thy_load.ML	Wed Feb 03 20:25:53 1999 +0100
@@ -20,7 +20,7 @@
   val find_file: Path.T -> (Path.T * File.info) option
   val check_file: Path.T -> File.info option
   val load_file: Path.T -> File.info
-  val check_thy: string -> File.info
+  val check_thy: string -> bool -> File.info
   val deps_thy: string -> bool -> File.info * (string list * Path.T list)
   val load_thy: string -> bool -> bool -> File.info
 end;
@@ -86,7 +86,13 @@
 val deps_thy_fn = ref (undefined: string -> bool -> Path.T -> string list * Path.T list);
 val load_thy_fn = ref (undefined: string -> bool -> bool -> Path.T -> unit);
 
-val check_thy = #1 o process_thy (K ());
+fun check_thy name ml =
+  let val (thy_info, _) = process_thy (K ()) name in
+    (case if ml then check_file (ml_path name) else None of
+      None => thy_info
+    | Some info => File.join_info thy_info info)
+  end;
+
 fun deps_thy name ml = process_thy (fn path => ! deps_thy_fn name ml path) name;
 fun load_thy name ml time = #1 (process_thy (fn path => ! load_thy_fn name ml time path) name);