clarified;
authorwenzelm
Sat Apr 08 21:09:34 2017 +0200 (2017-04-08 ago)
changeset 654421ca6d8a2a00d
parent 65441 9425e4d8bdb6
child 65443 dccbfc715904
clarified;
src/Pure/PIDE/resources.ML
     1.1 --- a/src/Pure/PIDE/resources.ML	Sat Apr 08 20:56:41 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Sat Apr 08 21:09:34 2017 +0200
     1.3 @@ -103,11 +103,10 @@
     1.4  fun check_thy dir thy_name =
     1.5    let
     1.6      val thy_base_name = Long_Name.base_name thy_name;
     1.7 -    val thy_path = thy_path (Path.basic thy_base_name);
     1.8      val master_file =
     1.9        (case known_theory thy_name of
    1.10 -        NONE => check_file dir thy_path
    1.11 -      | SOME known_path => check_file Path.current known_path);
    1.12 +        SOME known_path => check_file Path.current known_path
    1.13 +      | NONE => check_file dir (thy_path (Path.basic thy_base_name)));
    1.14      val text = File.read master_file;
    1.15  
    1.16      val {name = (name, pos), imports, keywords} =
    1.17 @@ -115,7 +114,7 @@
    1.18      val _ =
    1.19        thy_base_name <> name andalso
    1.20          error ("Bad theory name " ^ quote name ^
    1.21 -          " for file " ^ Path.print thy_path ^ Position.here pos);
    1.22 +          " for file " ^ Path.print (Path.base master_file) ^ Position.here pos);
    1.23    in
    1.24     {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
    1.25      imports = imports, keywords = keywords}