--- 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 =
{