src/Pure/Thy/sessions.scala
changeset 66737 2edc0c42c883
parent 66736 148891036469
child 66742 b3422f78270e
     1.1 --- a/src/Pure/Thy/sessions.scala	Sun Oct 01 12:28:52 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sun Oct 01 13:07:31 2017 +0200
     1.3 @@ -368,6 +368,7 @@
     1.4    sealed case class Selection(
     1.5      requirements: Boolean = false,
     1.6      all_sessions: Boolean = false,
     1.7 +    base_sessions: List[String] = Nil,
     1.8      exclude_session_groups: List[String] = Nil,
     1.9      exclude_sessions: List[String] = Nil,
    1.10      session_groups: List[String] = Nil,
    1.11 @@ -377,6 +378,7 @@
    1.12        Selection(
    1.13          requirements = requirements || other.requirements,
    1.14          all_sessions = all_sessions || other.all_sessions,
    1.15 +        base_sessions = Library.merge(base_sessions, other.base_sessions),
    1.16          exclude_session_groups = Library.merge(exclude_session_groups, other.exclude_session_groups),
    1.17          exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions),
    1.18          session_groups = Library.merge(session_groups, other.session_groups),
    1.19 @@ -385,8 +387,10 @@
    1.20      def apply(graph: Graph[String, Info]): (List[String], Graph[String, Info]) =
    1.21      {
    1.22        val bad_sessions =
    1.23 -        SortedSet((exclude_sessions ::: sessions).filterNot(graph.defined(_)): _*).toList
    1.24 -      if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
    1.25 +        SortedSet((base_sessions ::: exclude_sessions ::: sessions).
    1.26 +          filterNot(graph.defined(_)): _*).toList
    1.27 +      if (bad_sessions.nonEmpty)
    1.28 +        error("Undefined session(s): " + commas_quote(bad_sessions))
    1.29  
    1.30        val excluded =
    1.31        {
    1.32 @@ -404,7 +408,7 @@
    1.33          if (all_sessions) graph.keys
    1.34          else {
    1.35            val select_group = session_groups.toSet
    1.36 -          val select = sessions.toSet
    1.37 +          val select = sessions.toSet ++ graph.all_succs(base_sessions)
    1.38            (for {
    1.39              (name, (info, _)) <- graph.iterator
    1.40              if info.select || select(name) || graph.get_node(name).groups.exists(select_group)