src/Pure/Thy/sessions.scala

     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
   }
 
   object Selection
   {
-    val all: Selection = Selection(all_sessions = true)
+    val empty: Selection = Selection()
   }
 
   sealed case class Selection(
     requirements: Boolean = false,
     all_sessions: Boolean = false,
     exclude_session_groups: List[String] = Nil,
     exclude_sessions: List[String] = Nil,
     session_groups: List[String] = Nil,
     sessions: List[String] = Nil)
   {
+    def + (other: Selection): Selection =
+      Selection(
+        requirements = requirements || other.requirements,
+        all_sessions = all_sessions || other.all_sessions,
+        exclude_session_groups = exclude_session_groups ::: other.exclude_session_groups,
+        exclude_sessions = exclude_sessions ::: other.exclude_sessions,
+        session_groups = session_groups ::: other.session_groups,
+        sessions = sessions ::: other.sessions)
+
     def apply(graph: Graph[String, Info]): (List[String], Graph[String, Info]) =
     {
       val bad_sessions =
         SortedSet((exclude_sessions ::: sessions).filterNot(graph.defined(_)): _*).toList
       if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))