src/Pure/PIDE/resources.ML
changeset 65454 2b22b7d8649f
parent 65445 e9e7f5f5794c
child 65457 2bf0d2fcd506
     1.1 --- a/src/Pure/PIDE/resources.ML	Mon Apr 10 11:50:15 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Mon Apr 10 11:52:21 2017 +0200
     1.3 @@ -20,7 +20,8 @@
     1.4    val imports_of: theory -> (string * Position.T) list
     1.5    val thy_path: Path.T -> Path.T
     1.6    val theory_qualifier: string -> string
     1.7 -  val import_name: string -> Path.T -> Path.T -> {node_name: Path.T, theory_name: string}
     1.8 +  val import_name: string -> Path.T -> string ->
     1.9 +    {node_name: Path.T, master_dir: Path.T, theory_name: string}
    1.10    val check_thy: Path.T -> string ->
    1.11     {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
    1.12      imports: (string * Position.T) list, keywords: Thy_Header.keywords}
    1.13 @@ -105,9 +106,9 @@
    1.14  fun theory_qualifier theory =
    1.15    Long_Name.qualifier theory;
    1.16  
    1.17 -fun import_name qualifier dir path =
    1.18 +fun import_name qualifier dir s =
    1.19    let
    1.20 -    val theory0 = Path.implode (Path.base path);
    1.21 +    val theory0 = Thy_Header.import_name s;
    1.22      val theory =
    1.23        if Long_Name.is_qualified theory0 orelse global_theory theory0
    1.24          orelse true (* FIXME *) then theory0
    1.25 @@ -118,8 +119,8 @@
    1.26           fn () => loaded_theory theory0,
    1.27           fn () => known_theory theory,
    1.28           fn () => known_theory theory0,
    1.29 -         fn () => SOME (File.full_path dir (thy_path path))])
    1.30 -  in {node_name = node_name, theory_name = theory} end;
    1.31 +         fn () => SOME (File.full_path dir (thy_path (Path.expand (Path.explode s))))])
    1.32 +  in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end;
    1.33  
    1.34  fun check_file dir file = File.check_file (File.full_path dir file);
    1.35