src/Pure/Thy/sessions.scala
changeset 65540 2b73ed8bf4d9
parent 65532 febfd9f78bd4
child 65560 327842649e8d
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri Apr 21 17:34:13 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri Apr 21 18:51:24 2017 +0200
     1.3 @@ -98,6 +98,7 @@
     1.4    }
     1.5  
     1.6    sealed case class Base(
     1.7 +    imports: Option[Base] = None,
     1.8      global_theories: Map[String, String] = Map.empty,
     1.9      loaded_theories: Map[String, String] = Map.empty,
    1.10      known: Known = Known.empty,
    1.11 @@ -106,6 +107,8 @@
    1.12      sources: List[(Path, SHA1.Digest)] = Nil,
    1.13      session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
    1.14    {
    1.15 +    def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
    1.16 +
    1.17      def platform_path: Base = copy(known = known.platform_path)
    1.18  
    1.19      def loaded_theory(name: Document.Node.Name): Boolean =
    1.20 @@ -237,7 +240,8 @@
    1.21              }
    1.22  
    1.23              val base =
    1.24 -              Base(global_theories = global_theories,
    1.25 +              Base(imports = Some(imports_base),
    1.26 +                global_theories = global_theories,
    1.27                  loaded_theories = thy_deps.loaded_theories,
    1.28                  known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
    1.29                  keywords = thy_deps.keywords,