# HG changeset patch
# User wenzelm
# Date 918491544 -3600
# Node ID f30d1e31b9df8ff6bd435c3b16c557f47ebb74e9
# Parent  0ebfcf181d8480445d3d0a3bbc0dfb7c913f01ed
tuned msgs;

diff -r 0ebfcf181d84 -r f30d1e31b9df src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Feb 08 17:32:06 1999 +0100
+++ b/src/Pure/Thy/thy_info.ML	Mon Feb 08 17:32:24 1999 +0100
@@ -215,8 +215,8 @@
     val missing_files = mapfilter (fn (path, None) => Some (Path.pack path) | _ => None) files;
   in
     if null missing_files then ()
-    else warning (loader_msg ("unresolved dependencies on file(s) " ^ commas_quote missing_files ^
-      "\nfor theory") [name]);
+    else warning (loader_msg "unresolved dependencies of theory" [name] ^
+      "\nfile(s): " ^ commas_quote missing_files);
     change_deps name (fn _ => Some (make_deps true false master files))
   end;
 
@@ -226,11 +226,10 @@
 fun run_file path =
   let
     fun provide name info (deps as Some {present, outdated, master, files}) =
-          if present then deps
-          else if exists (equal path o #1) files then
+          if exists (equal path o #1) files then
             Some (make_deps present outdated master (overwrite (files, (path, Some info))))
           else (warning (loader_msg "undeclared dependency of theory" [name] ^
-            ": " ^ quote (Path.pack path)); deps)
+            "\nfile: " ^ quote (Path.pack path)); deps)
       | provide _ _ None = None;
   in
     (case apsome PureThy.get_name (Context.get_context ()) of