src/Pure/Thy/sessions.scala
changeset 66736 148891036469
parent 66722 9c661b74ce92
child 66737 2edc0c42c883
     1.1 --- a/src/Pure/Thy/sessions.scala	Sat Sep 30 22:55:23 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sun Oct 01 12:28:52 2017 +0200
     1.3 @@ -373,14 +373,14 @@
     1.4      session_groups: List[String] = Nil,
     1.5      sessions: List[String] = Nil)
     1.6    {
     1.7 -    def + (other: Selection): Selection =
     1.8 +    def ++ (other: Selection): Selection =
     1.9        Selection(
    1.10          requirements = requirements || other.requirements,
    1.11          all_sessions = all_sessions || other.all_sessions,
    1.12 -        exclude_session_groups = exclude_session_groups ::: other.exclude_session_groups,
    1.13 -        exclude_sessions = exclude_sessions ::: other.exclude_sessions,
    1.14 -        session_groups = session_groups ::: other.session_groups,
    1.15 -        sessions = sessions ::: other.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 +        sessions = Library.merge(sessions, other.sessions))
    1.20  
    1.21      def apply(graph: Graph[String, Info]): (List[String], Graph[String, Info]) =
    1.22      {