more uniform checks;
authorwenzelm
Wed, 01 Aug 2018 19:48:58 +0200
changeset 68733 76e339ef60e3
parent 68732 5472f4409fe6
child 68734 c14a2cc9b5ef
more uniform checks;
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 =
       {