# HG changeset patch
# User wenzelm
# Date 935001729 -7200
# Node ID 96f71fb54efb4f04626eff9aeacf5213b6f6e729
# Parent  28d95a7a265abbce161e91da84b6f3a6a452aac2
deps: include 'really' flag;

diff -r 28d95a7a265a -r 96f71fb54efb src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Aug 18 20:41:16 1999 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Aug 18 20:42:09 1999 +0200
@@ -30,7 +30,7 @@
   val names: unit -> string list
   val get_theory: string -> theory
   val get_preds: string -> string list
-  val loaded_files: string -> (Path.T * File.info) list
+  val loaded_files: string -> ((Path.T * File.info) * bool) list
   val touch_all_thys: unit -> unit
   val may_load_file: bool -> bool -> Path.T -> unit
   val use_path: Path.T -> unit
@@ -93,7 +93,7 @@
 
 type deps =
   {present: bool, outdated: bool,
-    master: ThyLoad.master option, files: (Path.T * (Path.T * File.info) option) list};
+    master: ThyLoad.master option, files: (Path.T * ((Path.T * File.info) * bool) option) list};
 
 fun make_deps present outdated master files =
   {present = present, outdated = outdated, master = master, files = files}: deps;
@@ -140,7 +140,7 @@
 
 fun loaded_files name =
   (case get_deps name of
-    Some {master = Some master, files, ...} => ThyLoad.get_thy master :: mapfilter #2 files
+    Some {master = Some master, files, ...} => (ThyLoad.get_thy master, true) :: mapfilter #2 files
   | Some {files, ...} => mapfilter #2 files
   | None => []);
 
@@ -207,7 +207,8 @@
     val load = ThyLoad.may_load_file really;
     fun provide name info (deps as Some {present, outdated, master, files}) =
           if exists (equal path o #1) files then
-            Some (make_deps present outdated master (overwrite (files, (path, Some info))))
+            Some (make_deps present outdated master
+              (overwrite (files, (path, Some (info, really)))))
           else (warning (loader_msg "undeclared dependency of theory" [name] ^
             " on file: " ^ quote (Path.pack path)); deps)
       | provide _ _ None = None;
@@ -272,7 +273,7 @@
   in (Some (init_deps (Some master) files), parents) end;
 
 fun file_current (_, None) = false
-  | file_current (path, info) = info = ThyLoad.check_file path;
+  | file_current (path, info) = (apsome fst info = ThyLoad.check_file path);
 
 fun current_deps strict dir name =
   (case lookup_deps name of