# HG changeset patch
# User wenzelm
# Date 1530284017 -7200
# Node ID 02df6c68a8cb4c9a00e201e3ecdb89c490a6fa02
# Parent  12b4b3bc585d8ede473db256a2dc0d7bb921306e
clarified error;

diff -r 12b4b3bc585d -r 02df6c68a8cb src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Jun 29 16:45:54 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Jun 29 16:53:37 2018 +0200
@@ -461,7 +461,11 @@
     {
       val sel_sessions1 = session1 :: session :: include_sessions
       val select_sessions1 =
-        if (session_focus) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1
+        if (session_focus) {
+          full_sessions1.check_sessions(sel_sessions1)
+          full_sessions1.imports_descendants(sel_sessions1)
+        }
+        else sel_sessions1
       full_sessions1.selection(Selection(sessions = select_sessions1))
     }
 
@@ -679,13 +683,16 @@
               }
           })
 
+    def check_sessions(names: List[String])
+    {
+      val bad_sessions = SortedSet(names.filterNot(defined(_)): _*).toList
+      if (bad_sessions.nonEmpty)
+        error("Undefined session(s): " + commas_quote(bad_sessions))
+    }
+
     def selection(sel: Selection): Structure =
     {
-      val bad_sessions =
-        SortedSet((sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions).
-          filterNot(defined(_)): _*).toList
-      if (bad_sessions.nonEmpty)
-        error("Undefined session(s): " + commas_quote(bad_sessions))
+      check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
 
       val excluded = sel.excluded(build_graph).toSet