# HG changeset patch
# User wenzelm
# Date 1510071413 -3600
# Node ID c4e678c2df3c0eba8949bf9cbdc5b3d6b3f09597
# Parent  d4f245bea0817f9d38c76ebd597871c3ffedd765
clarified exclusion: operate on completed selection, as last step;

diff -r d4f245bea081 -r c4e678c2df3c src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Nov 07 17:21:39 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 17:16:53 2017 +0100
@@ -609,13 +609,15 @@
               if info.dir_selected || select_session(name) || apply(name).groups.exists(select_group)
             } yield name).toList
           }
-        }.filterNot(excluded)
+        }
 
         val selected1 =
           if (sel.requirements) (graph.all_preds(selected0).toSet -- selected0).toList
           else selected0
 
-        graph.restrict(graph.all_preds(selected1).toSet)
+        val selected2 = graph.all_preds(selected1).filterNot(excluded)
+
+        graph.restrict(graph.all_preds(selected2).toSet)
       }
 
       new T(restrict(build_graph), restrict(imports_graph))