tuned msgs;
authorwenzelm
Mon Feb 08 17:32:24 1999 +0100 (1999-02-08)
changeset 6263f30d1e31b9df
parent 6262 0ebfcf181d84
child 6264 87e5f5b40595
tuned msgs;
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Mon Feb 08 17:32:06 1999 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Feb 08 17:32:24 1999 +0100
     1.3 @@ -215,8 +215,8 @@
     1.4      val missing_files = mapfilter (fn (path, None) => Some (Path.pack path) | _ => None) files;
     1.5    in
     1.6      if null missing_files then ()
     1.7 -    else warning (loader_msg ("unresolved dependencies on file(s) " ^ commas_quote missing_files ^
     1.8 -      "\nfor theory") [name]);
     1.9 +    else warning (loader_msg "unresolved dependencies of theory" [name] ^
    1.10 +      "\nfile(s): " ^ commas_quote missing_files);
    1.11      change_deps name (fn _ => Some (make_deps true false master files))
    1.12    end;
    1.13  
    1.14 @@ -226,11 +226,10 @@
    1.15  fun run_file path =
    1.16    let
    1.17      fun provide name info (deps as Some {present, outdated, master, files}) =
    1.18 -          if present then deps
    1.19 -          else if exists (equal path o #1) files then
    1.20 +          if exists (equal path o #1) files then
    1.21              Some (make_deps present outdated master (overwrite (files, (path, Some info))))
    1.22            else (warning (loader_msg "undeclared dependency of theory" [name] ^
    1.23 -            ": " ^ quote (Path.pack path)); deps)
    1.24 +            "\nfile: " ^ quote (Path.pack path)); deps)
    1.25        | provide _ _ None = None;
    1.26    in
    1.27      (case apsome PureThy.get_name (Context.get_context ()) of