src/Pure/PIDE/resources.ML
changeset 65433 a260181505c1
parent 65431 4a3e6cda3b94
child 65441 9425e4d8bdb6
     1.1 --- a/src/Pure/PIDE/resources.ML	Fri Apr 07 20:25:01 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Fri Apr 07 21:06:48 2017 +0200
     1.3 @@ -82,15 +82,20 @@
     1.4  
     1.5  fun check_thy dir thy_name =
     1.6    let
     1.7 -    val path = thy_path (Path.basic thy_name);
     1.8 -    val master_file = check_file dir path;
     1.9 +    val thy_base_name = Long_Name.base_name thy_name;
    1.10 +    val thy_path = thy_path (Path.basic thy_base_name);
    1.11 +    val master_file =
    1.12 +      (case known_theory thy_name of
    1.13 +        NONE => check_file dir thy_path
    1.14 +      | SOME known_path => check_file Path.current known_path);
    1.15      val text = File.read master_file;
    1.16  
    1.17      val {name = (name, pos), imports, keywords} =
    1.18        Thy_Header.read (Path.position master_file) text;
    1.19 -    val _ = thy_name <> name andalso
    1.20 -      error ("Bad theory name " ^ quote name ^
    1.21 -        " for file " ^ Path.print path ^ Position.here pos);
    1.22 +    val _ =
    1.23 +      thy_base_name <> name andalso
    1.24 +        error ("Bad theory name " ^ quote name ^
    1.25 +          " for file " ^ Path.print thy_path ^ Position.here pos);
    1.26    in
    1.27     {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
    1.28      imports = imports, keywords = keywords}