src/Pure/Thy/sessions.scala

     }
   }
 
   object Base
   {
-    def bootstrap(global_theories: Map[String, String]): Base =
+    def bootstrap(
+        session_directories: Map[JFile, (String, Boolean)],
+        global_theories: Map[String, String]): Base =
       Base(
+        session_directories = session_directories,
         global_theories = global_theories,
         overall_syntax = Thy_Header.bootstrap_syntax)
   }
 
   sealed case class Base(
     pos: Position.T = Position.none,
     doc_names: List[String] = Nil,
+    session_directories: Map[JFile, (String, Boolean)] = Map.empty,
     global_theories: Map[String, String] = Map.empty,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
     used_theories: List[((Document.Node.Name, Options), List[Document.Node.Name])] = Nil,
     dump_checkpoints: Set[Document.Node.Name] = Set.empty,
     known: Known = Known.empty,

 
     def dest_known_theories: List[(String, String)] =
       for ((theory, entry) <- known.theories.toList)
         yield (theory, entry.name.node)
 
-    def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
+    def get_imports: Base =
+      imports getOrElse Base.bootstrap(session_directories, global_theories)
   }
 
   sealed case class Deps(
     sessions_structure: Structure, session_bases: Map[String, Base], all_known: Known)
   {

 
           val info = sessions_structure(session_name)
           try {
             val parent_base: Sessions.Base =
               info.parent match {
-                case None => Base.bootstrap(sessions_structure.global_theories)
+                case None =>
+                  Base.bootstrap(
+                    sessions_structure.session_directories,
+                    sessions_structure.global_theories)
                 case Some(parent) => session_bases(parent)
               }
             val imports_base: Sessions.Base =
               parent_base.copy(known =
                 Known.make(info.dir, parent_base :: info.imports.map(session_bases(_))))

 
             val base =
               Base(
                 pos = info.pos,
                 doc_names = doc_names,
+                session_directories = sessions_structure.session_directories,
                 global_theories = sessions_structure.global_theories,
                 loaded_theories = dependencies.loaded_theories,
                 used_theories = used_theories,
                 dump_checkpoints = dump_checkpoints,
                 known = known,