src/Pure/Thy/thy_info.ML

  {master: (Path.T * SHA1.digest),  (*master dependencies for thy file*)
   imports: (string * Position.T) list};  (*source specification of imports (partially qualified)*)
 
 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
   val global_thys =
     Synchronized.var "Thy_Info.thys"

 
 (* access deps *)
 
 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 *)
 
 fun lookup_theory name =

 in
 
 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 =
-  let
-    val path = Path.expand (Path.explode str);
-    val {node_name, theory_name} = Resources.import_name qualifier dir path;
+and require_thy document symbols last_timing initiators qualifier dir (s, require_pos) tasks =
+  let
+    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 ()
           else
             error ("Incoherent imports for theory " ^ quote theory_name ^

   in
     (case try (String_Graph.get_node tasks) theory_name of
       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 ^
                   Position.here require_pos ^ required_by "\n" initiators);
 
           val parents = map (Thy_Header.import_name o #1) imports;
           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 =
             if all_current then Finished (get_theory theory_name)
             else