--- a/src/Pure/Thy/sessions.scala Tue Sep 26 16:12:21 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Tue Sep 26 17:32:16 2017 +0200
@@ -106,7 +106,6 @@
sealed case class Base(
pos: Position.T = Position.none,
- imports: Option[Base] = None,
global_theories: Map[String, String] = Map.empty,
loaded_theories: Map[String, String] = Map.empty,
known: Known = Known.empty,
@@ -114,10 +113,9 @@
syntax: Outer_Syntax = Outer_Syntax.empty,
sources: List[(Path, SHA1.Digest)] = Nil,
session_graph: Graph_Display.Graph = Graph_Display.empty_graph,
- errors: List[String] = Nil)
+ errors: List[String] = Nil,
+ imports: Option[Base] = None)
{
- def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
-
def platform_path: Base = copy(known = known.platform_path)
def standard_path: Base = copy(known = known.standard_path)
@@ -130,6 +128,8 @@
def dest_known_theories: List[(String, String)] =
for ((theory, node_name) <- known.theories.toList)
yield (theory, node_name.node)
+
+ def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
}
sealed case class Deps(session_bases: Map[String, Base], all_known: Known)
@@ -265,7 +265,6 @@
val base =
Base(
pos = info.pos,
- imports = Some(imports_base),
global_theories = global_theories,
loaded_theories = thy_deps.loaded_theories,
known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
@@ -273,7 +272,8 @@
syntax = syntax,
sources = sources,
session_graph = session_graph,
- errors = thy_deps.errors ::: sources_errors)
+ errors = thy_deps.errors ::: sources_errors,
+ imports = Some(imports_base))
session_bases + (info.name -> base)
}