check_file: fall back on Path.current;
authorwenzelm
Fri, 20 Jul 2007 19:54:03 +0200
changeset 238909a75e9772761
parent 23889 1794f405eacc
child 23891 4127c1d910f1
check_file: fall back on Path.current;
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Thy/thy_load.ML	Fri Jul 20 19:13:07 2007 +0200
     1.2 +++ b/src/Pure/Thy/thy_load.ML	Fri Jul 20 19:54:03 2007 +0200
     1.3 @@ -75,9 +75,11 @@
     1.4        let val ext_path = Path.expand (Path.ext ext rel_path)
     1.5        in Option.map (fn id => (File.full_path ext_path, id)) (File.ident ext_path) end;
     1.6      fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);
     1.7 -
     1.8 -    val via_load_path = if Path.is_basic path then get_first try_prfx (! load_path) else NONE;
     1.9 -  in (case via_load_path of NONE => try_prfx dir | res => res) end;
    1.10 +  in
    1.11 +    (case get_first try_prfx (if Path.is_basic path then (! load_path) else [Path.current]) of
    1.12 +      NONE => try_prfx dir
    1.13 +    | res => res)
    1.14 +  end;
    1.15  
    1.16  val check_file = check_ext [];
    1.17  val check_ml = check_ext ml_exts;