src/Pure/Thy/sessions.scala
changeset 66990 b23adab22e67
parent 66988 7f8c1dd7576a
child 66991 fc87d3becd69
     1.1 --- a/src/Pure/Thy/sessions.scala	Thu Nov 02 11:26:58 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Thu Nov 02 11:47:32 2017 +0100
     1.3 @@ -346,7 +346,8 @@
     1.4      val full_sessions = load(options, dirs = dirs)
     1.5      val global_theories = full_sessions.global_theories
     1.6  
     1.7 -    val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
     1.8 +    val selected_sessions =
     1.9 +      full_sessions.selection(Selection(sessions = session :: ancestor_session.toList))._2
    1.10      val info = selected_sessions(session)
    1.11      val ancestor = ancestor_session orElse info.parent
    1.12  
    1.13 @@ -357,9 +358,11 @@
    1.14  
    1.15          val ancestor_loaded =
    1.16            deps.get(ancestor.get) match {
    1.17 -            case None =>
    1.18 +            case Some(ancestor_base)
    1.19 +            if !selected_sessions.imports_requirements(List(ancestor.get)).contains(session) =>
    1.20 +              ancestor_base.loaded_theories.defined(_)
    1.21 +            case _ =>
    1.22                error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session))
    1.23 -            case Some(ancestor_base) => ancestor_base.loaded_theories.defined(_)
    1.24            }
    1.25  
    1.26          val required_theories =