clarified exclusion: operate on completed selection, as last step;
authorwenzelm
Tue Nov 07 17:16:53 2017 +0100 (19 months ago)
changeset 67028c4e678c2df3c
parent 67027 d4f245bea081
child 67029 d6d9fd2559ce
clarified exclusion: operate on completed selection, as last step;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Nov 07 17:21:39 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 17:16:53 2017 +0100
     1.3 @@ -609,13 +609,15 @@
     1.4                if info.dir_selected || select_session(name) || apply(name).groups.exists(select_group)
     1.5              } yield name).toList
     1.6            }
     1.7 -        }.filterNot(excluded)
     1.8 +        }
     1.9  
    1.10          val selected1 =
    1.11            if (sel.requirements) (graph.all_preds(selected0).toSet -- selected0).toList
    1.12            else selected0
    1.13  
    1.14 -        graph.restrict(graph.all_preds(selected1).toSet)
    1.15 +        val selected2 = graph.all_preds(selected1).filterNot(excluded)
    1.16 +
    1.17 +        graph.restrict(graph.all_preds(selected2).toSet)
    1.18        }
    1.19  
    1.20        new T(restrict(build_graph), restrict(imports_graph))