src/Pure/PIDE/resources.ML
changeset 65443 dccbfc715904
parent 65442 1ca6d8a2a00d
child 65445 e9e7f5f5794c
     1.1 --- a/src/Pure/PIDE/resources.ML	Sat Apr 08 21:09:34 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Sat Apr 08 21:28:19 2017 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4    val master_directory: theory -> Path.T
     1.5    val imports_of: theory -> (string * Position.T) list
     1.6    val thy_path: Path.T -> Path.T
     1.7 +  val import_name: Path.T -> Path.T -> {node_name: Path.T, theory_name: string}
     1.8    val check_thy: Path.T -> string ->
     1.9     {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
    1.10      imports: (string * Position.T) list, keywords: Thy_Header.keywords}
    1.11 @@ -98,6 +99,21 @@
    1.12  
    1.13  val thy_path = Path.ext "thy";
    1.14  
    1.15 +fun import_name dir path =
    1.16 +  let
    1.17 +    val theory0 = Path.implode (Path.base path);
    1.18 +    val theory =
    1.19 +      if Long_Name.is_qualified theory0 orelse global_theory theory0 then theory0
    1.20 +      else Long_Name.qualify (default_qualifier ()) theory0;
    1.21 +    val node_name =
    1.22 +      the (get_first (fn e => e ())
    1.23 +        [fn () => loaded_theory theory,
    1.24 +         fn () => loaded_theory theory0,
    1.25 +         fn () => known_theory theory,
    1.26 +         fn () => known_theory theory0,
    1.27 +         fn () => SOME (File.full_path dir (thy_path path))])
    1.28 +  in {node_name = node_name, theory_name = theory} end;
    1.29 +
    1.30  fun check_file dir file = File.check_file (File.full_path dir file);
    1.31  
    1.32  fun check_thy dir thy_name =