src/Pure/Thy/sessions.scala
changeset 66988 7f8c1dd7576a
parent 66987 352b23c97ac8
child 66990 b23adab22e67
     1.1 --- a/src/Pure/Thy/sessions.scala	Thu Nov 02 10:16:22 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Thu Nov 02 11:25:37 2017 +0100
     1.3 @@ -152,6 +152,7 @@
     1.4    {
     1.5      def is_empty: Boolean = session_bases.isEmpty
     1.6      def apply(name: String): Base = session_bases(name)
     1.7 +    def get(name: String): Option[Base] = session_bases.get(name)
     1.8  
     1.9      def imported_sources(name: String): List[SHA1.Digest] =
    1.10        session_bases(name).imported_sources.map(_._2)
    1.11 @@ -337,6 +338,7 @@
    1.12  
    1.13    def base_info(options: Options, session: String,
    1.14      dirs: List[Path] = Nil,
    1.15 +    ancestor_session: Option[String] = None,
    1.16      all_known: Boolean = false,
    1.17      focus_session: Boolean = false,
    1.18      required_session: Boolean = false): Base_Info =
    1.19 @@ -346,24 +348,30 @@
    1.20  
    1.21      val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
    1.22      val info = selected_sessions(session)
    1.23 +    val ancestor = ancestor_session orElse info.parent
    1.24  
    1.25      val (session1, infos1) =
    1.26 -      if (required_session && info.parent.isDefined) {
    1.27 +      if (required_session && ancestor.isDefined) {
    1.28          val deps = Sessions.deps(selected_sessions, global_theories)
    1.29          val base = deps(session)
    1.30  
    1.31 -        val parent_loaded = deps(info.parent.get).loaded_theories.defined(_)
    1.32 +        val ancestor_loaded =
    1.33 +          deps.get(ancestor.get) match {
    1.34 +            case None =>
    1.35 +              error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session))
    1.36 +            case Some(ancestor_base) => ancestor_base.loaded_theories.defined(_)
    1.37 +          }
    1.38  
    1.39          val required_theories =
    1.40            for {
    1.41              thy <- base.loaded_theories.keys
    1.42 -            if !parent_loaded(thy) && base.theory_qualifier(thy) != session
    1.43 +            if !ancestor_loaded(thy) && base.theory_qualifier(thy) != session
    1.44            }
    1.45            yield thy
    1.46  
    1.47 -        if (required_theories.isEmpty) (info.parent.get, Nil)
    1.48 +        if (required_theories.isEmpty) (ancestor.get, Nil)
    1.49          else {
    1.50 -          val other_name = info.name + "(base)"
    1.51 +          val other_name = info.name + "_base(" + ancestor.get + ")"
    1.52            (other_name,
    1.53              List(
    1.54                make_info(info.options,
    1.55 @@ -375,7 +383,7 @@
    1.56                    name = other_name,
    1.57                    groups = info.groups,
    1.58                    path = ".",
    1.59 -                  parent = info.parent,
    1.60 +                  parent = ancestor,
    1.61                    description = "Required theory imports from other sessions",
    1.62                    options = Nil,
    1.63                    imports = info.imports,