# HG changeset patch
# User wenzelm
# Date 940525201 -7200
# Node ID e54db490c537fd2ddab583005e49077910e6f0e3
# Parent  824ea50b8dbb62e872836ff892a9c8bb91c1d0df
added known_thy;
added touch_child_thys;
tuned loaded_files;

diff -r 824ea50b8dbb -r e54db490c537 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Oct 21 18:59:25 1999 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Oct 21 19:00:01 1999 +0200
@@ -28,10 +28,12 @@
   val str_of_action: action -> string
   val add_hook: (action -> string -> unit) -> unit
   val names: unit -> string list
+  val known_thy: string -> bool
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
   val get_preds: string -> string list
-  val loaded_files: string -> ((Path.T * File.info) * bool) list
+  val loaded_files: string -> Path.T option * (Path.T * bool) list
+  val touch_child_thys: string -> unit
   val touch_all_thys: unit -> unit
   val may_load_file: bool -> bool -> Path.T -> unit
   val use_path: Path.T -> unit
@@ -121,6 +123,7 @@
 (* access thy *)
 
 fun lookup_thy name = Some (thy_graph Graph.get_node name) handle Graph.UNDEFINED _ => None;
+val known_thy = is_some o lookup_thy;
 
 fun get_thy name =
   (case lookup_thy name of
@@ -141,9 +144,10 @@
 
 fun loaded_files name =
   (case get_deps name of
-    Some {master = Some master, files, ...} => (ThyLoad.get_thy master, true) :: mapfilter #2 files
-  | Some {files, ...} => mapfilter #2 files
-  | None => []);
+    None => (None, [])
+  | Some {master, files, ...} =>
+      (apsome (#1 o ThyLoad.get_thy) master,
+        map (fn ((p, _), r) => (p, r)) (mapfilter #2 files)));
 
 fun get_preds name =
   (thy_graph Graph.imm_preds name) handle Graph.UNDEFINED _ =>
@@ -185,11 +189,17 @@
   else (change_deps name (apsome (fn {present, outdated = _, master, files} =>
     make_deps present true master files)); perform Outdate name);
 
+fun check_unfinished name =
+  if is_finished name then (warning (loader_msg "tried to touch finished theory" [name]); None)
+  else Some name;
+
 in
 
-fun touch_thy name =
-  if is_finished name then warning (loader_msg "tried to touch finished theory" [name])
-  else seq outdate_thy (thy_graph Graph.all_succs [name]);
+fun touch_thys names =
+  seq outdate_thy (thy_graph Graph.all_succs (mapfilter check_unfinished names));
+
+fun touch_thy name = touch_thys [name];
+fun touch_child_thys name = touch_thys (thy_graph Graph.imm_succs name);
 
 fun touch_all_thys () = seq outdate_thy (get_names ());
 
@@ -199,7 +209,7 @@
 (* check 'finished' state *)
 
 fun check_unfinished fail name =
-  if is_some (lookup_thy name) andalso is_finished name then
+  if known_thy name andalso is_finished name then
     fail (loader_msg "cannot update finished theory" [name])
   else ();
 
@@ -212,17 +222,17 @@
   let
     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
+          (if exists (equal path o #1) files then ()
+            else warning (loader_msg "undeclared dependency of theory" [name] ^
+              " on file: " ^ quote (Path.pack path));
             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)
+              (overwrite (files, (path, Some (info, really))))))
       | provide _ _ None = None;
   in
     (case apsome PureThy.get_name (Context.get_context ()) of
       None => (load path; ())
     | Some name =>
-        if is_some (lookup_thy name) then change_deps name (provide name (load path))
+        if known_thy name then change_deps name (provide name (load path))
         else (load path; ()))
   end;
 
@@ -348,8 +358,7 @@
 (* remove_thy *)
 
 fun remove_thy name =
-  if is_none (lookup_thy name) then warning (loader_msg "nothing known about theory" [name])
-  else if is_finished name then error (loader_msg "cannot remove finished theory" [name])
+  if is_finished name then error (loader_msg "cannot remove finished theory" [name])
   else
     let val succs = thy_graph Graph.all_succs [name] in
       writeln (loader_msg "removing" succs);