# HG changeset patch
# User wenzelm
# Date 1509619652 -3600
# Node ID b23adab22e6704e3a60d6d678ff2616d44a3c6c8
# Parent  25665e7775b7e4ba6dbd84e06bff05704c3da0bf
allow unrelated ancestor;
clarified error;

diff -r 25665e7775b7 -r b23adab22e67 NEWS
--- a/NEWS	Thu Nov 02 11:26:58 2017 +0100
+++ b/NEWS	Thu Nov 02 11:47:32 2017 +0100
@@ -44,7 +44,9 @@
   - option -S sets up the development environment to edit the
     specified session: it abbreviates -B -F -R -l
 
-  Example: isabelle jedit -A HOL -S Formal_SSA -d '$AFP'
+  Examples:
+    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
+    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
 
 
 *** HOL ***
diff -r 25665e7775b7 -r b23adab22e67 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Nov 02 11:26:58 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Nov 02 11:47:32 2017 +0100
@@ -346,7 +346,8 @@
     val full_sessions = load(options, dirs = dirs)
     val global_theories = full_sessions.global_theories
 
-    val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
+    val selected_sessions =
+      full_sessions.selection(Selection(sessions = session :: ancestor_session.toList))._2
     val info = selected_sessions(session)
     val ancestor = ancestor_session orElse info.parent
 
@@ -357,9 +358,11 @@
 
         val ancestor_loaded =
           deps.get(ancestor.get) match {
-            case None =>
+            case Some(ancestor_base)
+            if !selected_sessions.imports_requirements(List(ancestor.get)).contains(session) =>
+              ancestor_base.loaded_theories.defined(_)
+            case _ =>
               error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session))
-            case Some(ancestor_base) => ancestor_base.loaded_theories.defined(_)
           }
 
         val required_theories =