refer to known_theory;
authorwenzelm
Fri Apr 07 21:06:48 2017 +0200 (2017-04-07 ago)
changeset 65433a260181505c1
parent 65432 d938705819bb
child 65434 e62b1af601f0
refer to known_theory;
support for qualified theory name;
src/Pure/PIDE/resources.ML
     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}