check_file: secondary load path is legacy feature;
authorwenzelm
Wed Dec 29 13:51:17 2010 +0100 (2010-12-29)
changeset 4141235f30e07fe0d
parent 41411 3bcc3b9e1020
child 41413 64cd30d6b0b8
check_file: secondary load path is legacy feature;
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Thy/thy_load.ML	Wed Dec 29 12:37:15 2010 +0100
     1.2 +++ b/src/Pure/Thy/thy_load.ML	Wed Dec 29 13:51:17 2010 +0100
     1.3 @@ -165,13 +165,19 @@
     1.4        let val full_path = File.full_path (Path.append dir path) in
     1.5          (case file_ident full_path of
     1.6            NONE => NONE
     1.7 -        | SOME id => SOME (full_path, id))
     1.8 +        | SOME id => SOME (dir, (full_path, id)))
     1.9        end)
    1.10    end;
    1.11  
    1.12  fun check_file dirs file =
    1.13    (case get_file dirs file of
    1.14 -    SOME path_id => path_id
    1.15 +    SOME (_, path_id) =>
    1.16 +     (if is_some (get_file [hd dirs] file) then ()
    1.17 +      else
    1.18 +        legacy_feature ("File " ^ quote (Path.implode file) ^
    1.19 +          " located via secondary search path: " ^
    1.20 +          quote (Path.implode (#1 (the (get_file (tl dirs) file)))));
    1.21 +      path_id)
    1.22    | NONE => error ("Could not find file " ^ quote (Path.implode file) ^
    1.23        "\nin " ^ commas_quote (map Path.implode dirs)));
    1.24  
    1.25 @@ -219,7 +225,7 @@
    1.26      fun current (src_path, (_, id)) =
    1.27        (case get_file [master_dir] src_path of
    1.28          NONE => false
    1.29 -      | SOME (_, id') => id = id');
    1.30 +      | SOME (_, (_, id')) => id = id');
    1.31    in can check_loaded thy andalso forall current provided end;
    1.32  
    1.33  val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE))));