# HG changeset patch
# User wenzelm
# Date 1491817941 -7200
# Node ID 2b22b7d8649fad1aedab6ce403522ceab30d0d62
# Parent  b2562bdda54e990672fe5c67da0eee6c3388e6ec
clarified, according to Scala version;

diff -r b2562bdda54e -r 2b22b7d8649f src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Mon Apr 10 11:50:15 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Mon Apr 10 11:52:21 2017 +0200
@@ -20,7 +20,8 @@
   val imports_of: theory -> (string * Position.T) list
   val thy_path: Path.T -> Path.T
   val theory_qualifier: string -> string
-  val import_name: string -> Path.T -> Path.T -> {node_name: Path.T, theory_name: string}
+  val import_name: string -> Path.T -> string ->
+    {node_name: Path.T, master_dir: Path.T, theory_name: string}
   val check_thy: Path.T -> string ->
    {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
     imports: (string * Position.T) list, keywords: Thy_Header.keywords}
@@ -105,9 +106,9 @@
 fun theory_qualifier theory =
   Long_Name.qualifier theory;
 
-fun import_name qualifier dir path =
+fun import_name qualifier dir s =
   let
-    val theory0 = Path.implode (Path.base path);
+    val theory0 = Thy_Header.import_name s;
     val theory =
       if Long_Name.is_qualified theory0 orelse global_theory theory0
         orelse true (* FIXME *) then theory0
@@ -118,8 +119,8 @@
          fn () => loaded_theory theory0,
          fn () => known_theory theory,
          fn () => known_theory theory0,
-         fn () => SOME (File.full_path dir (thy_path path))])
-  in {node_name = node_name, theory_name = theory} end;
+         fn () => SOME (File.full_path dir (thy_path (Path.expand (Path.explode s))))])
+  in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end;
 
 fun check_file dir file = File.check_file (File.full_path dir file);
 
diff -r b2562bdda54e -r 2b22b7d8649f src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Apr 10 11:50:15 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Apr 10 11:52:21 2017 +0200
@@ -54,7 +54,7 @@
 
 fun make_deps master imports : deps = {master = master, imports = imports};
 
-fun master_dir (d: deps option) =
+fun master_dir_deps (d: deps option) =
   the_default Path.current (Option.map (Path.dir o #1 o #master) d);
 
 local
@@ -86,7 +86,7 @@
 
 val lookup_deps = Option.map #1 o lookup_thy;
 
-val master_directory = master_dir o #1 o get_thy;
+val master_directory = master_dir_deps o #1 o get_thy;
 
 
 (* access theory *)
@@ -287,10 +287,9 @@
 fun require_thys document symbols last_timing initiators qualifier dir strs tasks =
       fold_map (require_thy document symbols last_timing initiators qualifier dir) strs tasks
       |>> forall I
-and require_thy document symbols last_timing initiators qualifier dir (str, require_pos) tasks =
+and require_thy document symbols last_timing initiators qualifier dir (s, require_pos) tasks =
   let
-    val path = Path.expand (Path.explode str);
-    val {node_name, theory_name} = Resources.import_name qualifier dir path;
+    val {node_name, master_dir, theory_name} = Resources.import_name qualifier dir s;
     fun check_entry (Task (node_name', _, _)) =
           if op = (apply2 File.platform_path (node_name, node_name'))
           then ()
@@ -305,10 +304,9 @@
       SOME task => (check_entry task; (task_finished task, tasks))
     | NONE =>
         let
-          val dir' = Path.append dir (Path.dir path);
           val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators);
 
-          val (current, deps, theory_pos, imports, keywords) = check_deps dir' theory_name
+          val (current, deps, theory_pos, imports, keywords) = check_deps master_dir theory_name
             handle ERROR msg =>
               cat_error msg
                 ("The error(s) above occurred for theory " ^ quote theory_name ^
@@ -318,7 +316,7 @@
           val (parents_current, tasks') =
             require_thys document symbols last_timing (theory_name :: initiators)
               (Resources.theory_qualifier theory_name)
-              (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
+              (Path.append dir (master_dir_deps (Option.map #1 deps))) imports tasks;
 
           val all_current = current andalso parents_current;
           val task =