src/Pure/Thy/sessions.scala
changeset 68734 c14a2cc9b5ef
parent 68733 76e339ef60e3
child 68746 f95e2f145ea5
     1.1 --- a/src/Pure/Thy/sessions.scala	Wed Aug 01 19:48:58 2018 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Wed Aug 01 20:58:41 2018 +0200
     1.3 @@ -668,7 +668,7 @@
     1.4        check_sessions(sel)
     1.5  
     1.6        val select_group = sel.session_groups.toSet
     1.7 -      val select_session = sel.sessions.toSet ++ graph.all_succs(sel.base_sessions)
     1.8 +      val select_session = sel.sessions.toSet ++ imports_graph.all_succs(sel.base_sessions)
     1.9  
    1.10        val selected0 =
    1.11          if (sel.all_sessions) graph.keys
    1.12 @@ -693,10 +693,10 @@
    1.13          val exclude_group = sel.exclude_session_groups.toSet
    1.14          val exclude_group_sessions =
    1.15            (for {
    1.16 -            (name, (info, _)) <- build_graph.iterator
    1.17 -            if build_graph.get_node(name).groups.exists(exclude_group)
    1.18 +            (name, (info, _)) <- imports_graph.iterator
    1.19 +            if imports_graph.get_node(name).groups.exists(exclude_group)
    1.20            } yield name).toList
    1.21 -        build_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
    1.22 +        imports_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
    1.23        }
    1.24  
    1.25        def restrict(graph: Graph[String, Info]): Graph[String, Info] =