--- a/src/Pure/Thy/sessions.scala Mon Apr 03 14:29:44 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Mon Apr 03 16:36:45 2017 +0200
@@ -71,12 +71,12 @@
if (progress.stopped) throw Exn.Interrupt()
try {
- val resources =
- new Resources(
- info.parent match {
- case None => Base.bootstrap
- case Some(parent) => deps(parent)
- })
+ val parent_base =
+ info.parent match {
+ case None => Base.bootstrap
+ case Some(parent) => deps(parent)
+ }
+ val resources = new Resources(name, parent_base)
if (verbose || list_files) {
val groups =
@@ -91,10 +91,9 @@
info.theories.flatMap({
case (global, _, thys) =>
thys.map(thy =>
- (resources.node_name(
- if (global) "" else name, info.dir + resources.thy_path(thy)), info.pos))
+ (resources.init_name(global, info.dir + resources.thy_path(thy)), info.pos))
})
- val thy_deps = resources.thy_info.dependencies(name, root_theories)
+ val thy_deps = resources.thy_info.dependencies(root_theories)
thy_deps.errors match {
case Nil => thy_deps
@@ -103,7 +102,7 @@
}
val known_theories =
- (resources.base.known_theories /: thy_deps.deps)({ case (known, dep) =>
+ (parent_base.known_theories /: thy_deps.deps)({ case (known, dep) =>
val name = dep.name
known.get(name.theory) match {
case Some(name1) if name != name1 =>
@@ -142,7 +141,7 @@
val session_graph =
Present.session_graph(info.parent getOrElse "",
- resources.base.loaded_theories, thy_deps.deps)
+ parent_base.loaded_theories, thy_deps.deps)
val base =
Base(loaded_theories, known_theories, keywords, syntax, sources, session_graph)