# HG changeset patch
# User wenzelm
# Date 1507800306 -7200
# Node ID 982baed145422c15bd6eb6b3cf7bdf4fa0a4d94b
# Parent  e8282131ddf97079865d30fcdb42fbd98c4bc939
clarified signature;

diff -r e8282131ddf9 -r 982baed14542 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Thu Oct 12 05:37:58 2017 +0200
+++ b/src/Pure/ML/ml_process.scala	Thu Oct 12 11:25:06 2017 +0200
@@ -34,7 +34,7 @@
         val selection = Sessions.Selection(sessions = List(logic_name))
         val (_, selected_sessions) =
           sessions.getOrElse(Sessions.load(options, dirs)).selection(selection)
-        (selected_sessions.build_ancestors(logic_name) ::: List(logic_name)).
+        selected_sessions.build_requirements(List(logic_name)).
           map(a => File.platform_path(store.heap(a)))
       }
 
diff -r e8282131ddf9 -r 982baed14542 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Oct 12 05:37:58 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Oct 12 11:25:06 2017 +0200
@@ -509,18 +509,17 @@
       (selected, new T(build_graph1, imports_graph1))
     }
 
-    def build_ancestors(name: String): List[String] =
-      build_graph.all_preds(List(name)).tail.reverse
-
     def build_descendants(names: List[String]): List[String] =
       build_graph.all_succs(names)
-
+    def build_requirements(names: List[String]): List[String] =
+      build_graph.all_preds(names).reverse
     def build_topological_order: List[Info] =
       build_graph.topological_order.map(apply(_))
 
-    def imports_ancestors(name: String): List[String] =
-      imports_graph.all_preds(List(name)).tail.reverse
-
+    def imports_descendants(names: List[String]): List[String] =
+      imports_graph.all_succs(names)
+    def imports_requirements(names: List[String]): List[String] =
+      imports_graph.all_preds(names).reverse
     def imports_topological_order: List[Info] =
       imports_graph.topological_order.map(apply(_))
 
diff -r e8282131ddf9 -r 982baed14542 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Oct 12 05:37:58 2017 +0200
+++ b/src/Pure/Tools/build.scala	Thu Oct 12 11:25:06 2017 +0200
@@ -560,7 +560,9 @@
             //{{{ check/start next job
             pending.dequeue(running.isDefinedAt(_)) match {
               case Some((name, info)) =>
-                val ancestor_results = selected_sessions.build_ancestors(name).map(results(_))
+                val ancestor_results =
+                  selected_sessions.build_requirements(List(name)).filterNot(_ == name).
+                    map(results(_))
                 val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
 
                 val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
diff -r e8282131ddf9 -r 982baed14542 src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Thu Oct 12 05:37:58 2017 +0200
+++ b/src/Pure/Tools/imports.scala	Thu Oct 12 11:25:06 2017 +0200
@@ -99,8 +99,7 @@
         val info = full_sessions(session_name)
         val session_resources = new Resources(deps(session_name))
 
-        val declared_imports =
-          full_sessions.imports_ancestors(session_name).toSet + session_name
+        val declared_imports = full_sessions.imports_requirements(List(session_name)).toSet
         val extra_imports =
           (for {
             (_, a) <- session_resources.session_base.known.theories.iterator