src/Pure/Thy/sessions.scala
changeset 65359 9ca34f0407a9
parent 65355 403eabd73c9a
child 65360 3ff88fece1f6
--- 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)