src/Pure/Thy/sessions.scala
changeset 66694 41177b124067
parent 66668 6019cfb8256c
child 66696 8f863dae78a0
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Sep 26 16:12:21 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Sep 26 17:32:16 2017 +0200
     1.3 @@ -106,7 +106,6 @@
     1.4  
     1.5    sealed case class Base(
     1.6      pos: Position.T = Position.none,
     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 @@ -114,10 +113,9 @@
    1.12      syntax: Outer_Syntax = Outer_Syntax.empty,
    1.13      sources: List[(Path, SHA1.Digest)] = Nil,
    1.14      session_graph: Graph_Display.Graph = Graph_Display.empty_graph,
    1.15 -    errors: List[String] = Nil)
    1.16 +    errors: List[String] = Nil,
    1.17 +    imports: Option[Base] = None)
    1.18    {
    1.19 -    def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
    1.20 -
    1.21      def platform_path: Base = copy(known = known.platform_path)
    1.22      def standard_path: Base = copy(known = known.standard_path)
    1.23  
    1.24 @@ -130,6 +128,8 @@
    1.25      def dest_known_theories: List[(String, String)] =
    1.26        for ((theory, node_name) <- known.theories.toList)
    1.27          yield (theory, node_name.node)
    1.28 +
    1.29 +    def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
    1.30    }
    1.31  
    1.32    sealed case class Deps(session_bases: Map[String, Base], all_known: Known)
    1.33 @@ -265,7 +265,6 @@
    1.34              val base =
    1.35                Base(
    1.36                  pos = info.pos,
    1.37 -                imports = Some(imports_base),
    1.38                  global_theories = global_theories,
    1.39                  loaded_theories = thy_deps.loaded_theories,
    1.40                  known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
    1.41 @@ -273,7 +272,8 @@
    1.42                  syntax = syntax,
    1.43                  sources = sources,
    1.44                  session_graph = session_graph,
    1.45 -                errors = thy_deps.errors ::: sources_errors)
    1.46 +                errors = thy_deps.errors ::: sources_errors,
    1.47 +                imports = Some(imports_base))
    1.48  
    1.49              session_bases + (info.name -> base)
    1.50            }