more standard merge operation;
authorwenzelm
Sun Oct 01 12:28:52 2017 +0200 (21 months ago)
changeset 66736148891036469
parent 66735 5887ae5b95a8
child 66737 2edc0c42c883
more standard merge operation;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     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      {
     2.1 --- a/src/Pure/Tools/build.scala	Sat Sep 30 22:55:23 2017 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Sun Oct 01 12:28:52 2017 +0200
     2.3 @@ -372,7 +372,7 @@
     2.4      val (selected, selected_sessions) =
     2.5        full_sessions.selection(
     2.6            Sessions.Selection(requirements, all_sessions, exclude_session_groups,
     2.7 -            exclude_sessions, session_groups, sessions) + selection)
     2.8 +            exclude_sessions, session_groups, sessions) ++ selection)
     2.9  
    2.10      val deps =
    2.11        Sessions.deps(selected_sessions, progress = progress, inlined_files = true,