src/Pure/Thy/sessions.scala

--- a/src/Pure/Thy/sessions.scala	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Sep 12 13:33:09 2019 +0200
@@ -41,7 +41,6 @@
     val empty: Known = Known()
 
     def make(local_dir: Path, bases: List[Base],
-      sessions: List[(String, Position.T)] = Nil,
       theories: List[Document.Node.Entry] = Nil,
       loaded_files: List[(String, List[Path])] = Nil): Known =
     {
@@ -58,9 +57,6 @@
           entry.name.path.canonical_file.toPath.startsWith(local_path))
       }
 
-      val known_sessions =
-        (sessions.toMap /: bases)({ case (known, base) => known ++ base.known.sessions })
-
       val known_theories =
         (Map.empty[String, Document.Node.Entry] /: (bases_iterator(false) ++ theories.iterator))({
           case (known, entry) =>
@@ -92,7 +88,6 @@
         (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _)
 
       Known(
-        known_sessions,
         known_theories,
         known_theories_local,
         known_files.iterator.map(p => (p._1, p._2.reverse)).toMap,
@@ -101,7 +96,6 @@
   }
 
   sealed case class Known(
-    sessions: Map[String, Position.T] = Map.empty,
     theories: Map[String, Document.Node.Entry] = Map.empty,
     theories_local: Map[String, Document.Node.Entry] = Map.empty,
     files: Map[JFile, List[Document.Node.Name]] = Map.empty,
@@ -180,9 +174,6 @@
     def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax =
       nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
 
-    def known_theory(name: String): Option[Document.Node.Name] =
-      known.theories.get(name).map(_.name)
-
     def dest_known_theories: List[(String, String)] =
       for ((theory, entry) <- known.theories.toList)
         yield (theory, entry.name.node)
@@ -304,7 +295,7 @@
               parent_base.copy(known =
                 Known.make(info.dir, parent_base :: info.imports.map(session_bases(_))))
 
-            val resources = new Resources(imports_base)
+            val resources = new Resources(sessions_structure, imports_base)
 
             if (verbose || list_files) {
               val groups =
@@ -371,7 +362,6 @@
 
             val known =
               Known.make(info.dir, List(imports_base),
-                sessions = List(info.name -> info.pos),
                 theories = dependencies.entries,
                 loaded_files = loaded_files)
 
@@ -466,9 +456,7 @@
     dirs: List[Path] = Nil,
     include_sessions: List[String] = Nil,
     session_ancestor: Option[String] = None,
-    session_requirements: Boolean = false,
-    session_focus: Boolean = false,
-    all_known: Boolean = false): Base_Info =
+    session_requirements: Boolean = false): Base_Info =
   {
     val full_sessions = load_structure(options, dirs = dirs)
 
@@ -529,22 +517,11 @@
       else load_structure(options, dirs = dirs, infos = infos1)
 
     val selected_sessions1 =
-    {
-      val sel_sessions1 = session1 :: session :: include_sessions
-      val select_sessions1 =
-        if (session_focus) {
-          full_sessions1.check_sessions(sel_sessions1)
-          full_sessions1.imports_descendants(sel_sessions1)
-        }
-        else sel_sessions1
-      full_sessions1.selection(Selection(sessions = select_sessions1))
-    }
+      full_sessions1.selection(Selection(sessions = session1 :: session :: include_sessions))
 
-    val sessions1 = if (all_known) full_sessions1 else selected_sessions1
-    val deps1 = Sessions.deps(sessions1, progress = progress)
-    val base1 = deps1(session1).copy(known = deps1.all_known)
+    val deps1 = Sessions.deps(selected_sessions1, progress = progress)
 
-    Base_Info(options, dirs, session1, deps1.sessions_structure, deps1.errors, base1, infos1)
+    Base_Info(options, dirs, session1, full_sessions1, deps1.errors, deps1(session1), infos1)
   }
 
 
@@ -701,6 +678,9 @@
     val build_graph = add_edges(info_graph, "parent", _.parent)
     val imports_graph = add_edges(build_graph, "imports", _.imports)
 
+    val session_positions: List[(String, Position.T)] =
+      (for ((name, (info, _)) <- info_graph.iterator) yield (name, info.pos)).toList
+
     val session_directories: Map[JFile, String] =
       (Map.empty[JFile, String] /:
         (for {
@@ -735,10 +715,12 @@
             }
           })
 
-    new Structure(session_directories, global_theories, build_graph, imports_graph)
+    new Structure(
+      session_positions, session_directories, global_theories, build_graph, imports_graph)
   }
 
   final class Structure private[Sessions](
+      val session_positions: List[(String, Position.T)],
       val session_directories: Map[JFile, String],
       val global_theories: Map[String, String],
       val build_graph: Graph[String, Info],
@@ -746,6 +728,10 @@
   {
     sessions_structure =>
 
+    def dest_session_directories: List[(String, String)] =
+      for ((file, session) <- session_directories.toList)
+        yield (File.standard_path(file), session)
+
     lazy val chapters: SortedMap[String, List[Info]] =
       (SortedMap.empty[String, List[Info]] /: build_graph.iterator)(
         { case (chs, (_, (info, _))) =>
@@ -811,7 +797,8 @@
       }
 
       new Structure(
-        session_directories, global_theories, restrict(build_graph), restrict(imports_graph))
+        session_positions, session_directories, global_theories,
+        restrict(build_graph), restrict(imports_graph))
     }
 
     def selection_deps(