allow unrelated ancestor;
authorwenzelm
Thu Nov 02 11:47:32 2017 +0100 (17 months ago)
changeset 66990b23adab22e67
parent 66989 25665e7775b7
child 66991 fc87d3becd69
allow unrelated ancestor;
clarified error;
NEWS
src/Pure/Thy/sessions.scala
     1.1 --- a/NEWS	Thu Nov 02 11:26:58 2017 +0100
     1.2 +++ b/NEWS	Thu Nov 02 11:47:32 2017 +0100
     1.3 @@ -44,7 +44,9 @@
     1.4    - option -S sets up the development environment to edit the
     1.5      specified session: it abbreviates -B -F -R -l
     1.6  
     1.7 -  Example: isabelle jedit -A HOL -S Formal_SSA -d '$AFP'
     1.8 +  Examples:
     1.9 +    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
    1.10 +    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
    1.11  
    1.12  
    1.13  *** HOL ***
     2.1 --- a/src/Pure/Thy/sessions.scala	Thu Nov 02 11:26:58 2017 +0100
     2.2 +++ b/src/Pure/Thy/sessions.scala	Thu Nov 02 11:47:32 2017 +0100
     2.3 @@ -346,7 +346,8 @@
     2.4      val full_sessions = load(options, dirs = dirs)
     2.5      val global_theories = full_sessions.global_theories
     2.6  
     2.7 -    val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
     2.8 +    val selected_sessions =
     2.9 +      full_sessions.selection(Selection(sessions = session :: ancestor_session.toList))._2
    2.10      val info = selected_sessions(session)
    2.11      val ancestor = ancestor_session orElse info.parent
    2.12  
    2.13 @@ -357,9 +358,11 @@
    2.14  
    2.15          val ancestor_loaded =
    2.16            deps.get(ancestor.get) match {
    2.17 -            case None =>
    2.18 +            case Some(ancestor_base)
    2.19 +            if !selected_sessions.imports_requirements(List(ancestor.get)).contains(session) =>
    2.20 +              ancestor_base.loaded_theories.defined(_)
    2.21 +            case _ =>
    2.22                error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session))
    2.23 -            case Some(ancestor_base) => ancestor_base.loaded_theories.defined(_)
    2.24            }
    2.25  
    2.26          val required_theories =