src/Pure/Thy/sessions.scala
changeset 68733 76e339ef60e3
parent 68732 5472f4409fe6
child 68734 c14a2cc9b5ef
     1.1 --- a/src/Pure/Thy/sessions.scala	Wed Aug 01 19:38:06 2018 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Wed Aug 01 19:48:58 2018 +0200
     1.3 @@ -660,8 +660,13 @@
     1.4          error("Undefined session(s): " + commas_quote(bad_sessions))
     1.5      }
     1.6  
     1.7 +    def check_sessions(sel: Selection): Unit =
     1.8 +      check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
     1.9 +
    1.10      private def selected(graph: Graph[String, Info], sel: Selection): List[String] =
    1.11      {
    1.12 +      check_sessions(sel)
    1.13 +
    1.14        val select_group = sel.session_groups.toSet
    1.15        val select_session = sel.sessions.toSet ++ graph.all_succs(sel.base_sessions)
    1.16  
    1.17 @@ -681,7 +686,7 @@
    1.18  
    1.19      def selection(sel: Selection): Structure =
    1.20      {
    1.21 -      check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
    1.22 +      check_sessions(sel)
    1.23  
    1.24        val excluded =
    1.25        {