# HG changeset patch
# User wenzelm
# Date 1533145738 -7200
# Node ID 76e339ef60e3dc14e0a85d1cf1f891ab45a19cb0
# Parent  5472f4409fe67bbb472f93e9c7c9fcfe57fb27c7
more uniform checks;

diff -r 5472f4409fe6 -r 76e339ef60e3 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Aug 01 19:38:06 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Aug 01 19:48:58 2018 +0200
@@ -660,8 +660,13 @@
         error("Undefined session(s): " + commas_quote(bad_sessions))
     }
 
+    def check_sessions(sel: Selection): Unit =
+      check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
+
     private def selected(graph: Graph[String, Info], sel: Selection): List[String] =
     {
+      check_sessions(sel)
+
       val select_group = sel.session_groups.toSet
       val select_session = sel.sessions.toSet ++ graph.all_succs(sel.base_sessions)
 
@@ -681,7 +686,7 @@
 
     def selection(sel: Selection): Structure =
     {
-      check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
+      check_sessions(sel)
 
       val excluded =
       {