src/Pure/Thy/sessions.scala

     export_files: List[(Path, Int, List[String])],
     meta_digest: SHA1.Digest)
   {
     def deps: List[String] = parent.toList ::: imports
 
-    def dirs: List[Path] = dir :: directories.map(_._1)
-    def dirs_strict: List[Path] = dir :: (for { (d, false) <- directories } yield d)
+    def dirs: List[(Path, Boolean)] = (dir, false) :: directories
 
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
 
     def bibtex_entries: List[Text.Info[String]] =
       (for {

 
       if (exclude_session(name)) error("Bad session name")
       if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
       if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
 
+      val session_path = dir + Path.explode(entry.path)
       val directories =
-        for { (d, b) <- entry.directories }
-        yield (dir + Path.explode(d), b)
+        for { (dir, overlapping) <- entry.directories }
+        yield (session_path + Path.explode(dir), overlapping)
 
       val session_options = options ++ entry.options
 
       val theories =
         entry.theories.map({ case (opts, thys) =>

 
       val meta_digest =
         SHA1.digest((name, chapter, entry.parent, entry.directories, entry.options, entry.imports,
           entry.theories_no_position, conditions, entry.document_files).toString)
 
-      Info(name, chapter, dir_selected, entry.pos, entry.groups, dir + Path.explode(entry.path),
+      Info(name, chapter, dir_selected, entry.pos, entry.groups, session_path,
         entry.parent, entry.description, directories, session_options,
         entry.imports, theories, global_theories, document_files, export_files, meta_digest)
     }
     catch {
       case ERROR(msg) =>

           else graph.new_node(info.name, info)
       }
     val build_graph = add_edges(info_graph, "parent", _.parent)
     val imports_graph = add_edges(build_graph, "imports", _.imports)
 
-    val strict_directories: Map[JFile, String] =
-      (Map.empty[JFile, String] /:
+    val session_directories: Map[JFile, (String, Boolean)] =
+      (Map.empty[JFile, (String, Boolean)] /:
         (for {
           session <- imports_graph.topological_order.iterator
           info = info_graph.get_node(session)
-          dir <- info.dirs_strict.iterator
-        } yield (info, dir)))({ case (dirs, (info, dir)) =>
+          dir_overlapping <- info.dirs.iterator
+        } yield (info, dir_overlapping)))({ case (dirs, (info, (dir, overlapping))) =>
             val session = info.name
             val canonical_dir = dir.canonical_file
+            def update(over: Boolean) = dirs + (canonical_dir -> (session -> over))
             dirs.get(canonical_dir) match {
-              case Some(session1) if session != session1 =>
-                val info1 = info_graph.get_node(session1)
-                error("Duplicate use of directory " + dir +
-                  "\n  for session " + quote(session1) + Position.here(info1.pos) +
-                  "\n  vs. session " + quote(session) + Position.here(info.pos))
-              case _ => dirs + (canonical_dir -> session)
+              case Some((session1, overlapping1)) =>
+                if (session == session1) update(overlapping || overlapping1)
+                else if (overlapping && !overlapping1) dirs
+                else if (!overlapping && overlapping1) update(overlapping)
+                else {
+                  val info1 = info_graph.get_node(session1)
+                  error("Duplicate use of directory " + dir +
+                    "\n  for session " + quote(session1) + Position.here(info1.pos) +
+                    "\n  vs. session " + quote(session) + Position.here(info.pos))
+                }
+              case None => update(overlapping)
             }
           })
 
     val global_theories: Map[String, String] =
       (Thy_Header.bootstrap_global_theories.toMap /:

                 error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
               case _ => global + (thy -> qualifier)
             }
           })
 
-    new Structure(strict_directories, global_theories, build_graph, imports_graph)
+    new Structure(session_directories, global_theories, build_graph, imports_graph)
   }
 
   final class Structure private[Sessions](
-      val strict_directories: Map[JFile, String],
+      val session_directories: Map[JFile, (String, Boolean)],
       val global_theories: Map[String, String],
       val build_graph: Graph[String, Info],
       val imports_graph: Graph[String, Info])
   {
     sessions_structure =>

         val sessions = graph.all_preds(selected(graph, sel)).filterNot(excluded)
         graph.restrict(graph.all_preds(sessions).toSet)
       }
 
       new Structure(
-        strict_directories, global_theories, restrict(build_graph), restrict(imports_graph))
+        session_directories, global_theories, restrict(build_graph), restrict(imports_graph))
     }
 
     def selection_deps(
       options: Options,
       selection: Selection,