src/Pure/Thy/thy_load.ML
changeset 23890 9a75e9772761
parent 23885 09254a1622e3
child 23892 739707039b0d
equal deleted inserted replaced
23889:1794f405eacc 23890:9a75e9772761
    73 
    73 
    74     fun try_ext rel_path ext =
    74     fun try_ext rel_path ext =
    75       let val ext_path = Path.expand (Path.ext ext rel_path)
    75       let val ext_path = Path.expand (Path.ext ext rel_path)
    76       in Option.map (fn id => (File.full_path ext_path, id)) (File.ident ext_path) end;
    76       in Option.map (fn id => (File.full_path ext_path, id)) (File.ident ext_path) end;
    77     fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);
    77     fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);
    78 
    78   in
    79     val via_load_path = if Path.is_basic path then get_first try_prfx (! load_path) else NONE;
    79     (case get_first try_prfx (if Path.is_basic path then (! load_path) else [Path.current]) of
    80   in (case via_load_path of NONE => try_prfx dir | res => res) end;
    80       NONE => try_prfx dir
       
    81     | res => res)
       
    82   end;
    81 
    83 
    82 val check_file = check_ext [];
    84 val check_file = check_ext [];
    83 val check_ml = check_ext ml_exts;
    85 val check_ml = check_ext ml_exts;
    84 
    86 
    85 fun check_thy dir name ml =
    87 fun check_thy dir name ml =