# HG changeset patch
# User wenzelm
# Date 1491484845 -7200
# Node ID cc9e2f1f279d27eff38ccc1e6575f4eb2b26943a
# Parent  68f8a0dab28be6adc59bad9fbbbd842f8a2f360b
tuned signature;

diff -r 68f8a0dab28b -r cc9e2f1f279d src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Apr 06 14:41:56 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Apr 06 15:20:45 2017 +0200
@@ -42,31 +42,30 @@
       loaded_theories.contains(name.theory)
   }
 
-  sealed case class Deps(deps: Map[String, Base])
+  sealed case class Deps(sessions: Map[String, Base])
   {
-    def is_empty: Boolean = deps.isEmpty
-    def apply(name: String): Base = deps(name)
-    def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
+    def is_empty: Boolean = sessions.isEmpty
+    def apply(name: String): Base = sessions(name)
+    def sources(name: String): List[SHA1.Digest] = sessions(name).sources.map(_._2)
   }
 
-  def dependencies(
+  def deps(tree: Tree,
       progress: Progress = No_Progress,
       inlined_files: Boolean = false,
       verbose: Boolean = false,
       list_files: Boolean = false,
       check_keywords: Set[String] = Set.empty,
-      global_theories: Set[String] = Set.empty,
-      tree: Tree): Deps =
+      global_theories: Set[String] = Set.empty): Deps =
   {
     Deps((Map.empty[String, Base] /: tree.topological_order)(
-      { case (deps, (name, info)) =>
+      { case (sessions, (name, info)) =>
           if (progress.stopped) throw Exn.Interrupt()
 
           try {
             val parent_base =
               info.parent match {
                 case None => Base.bootstrap
-                case Some(parent) => deps(parent)
+                case Some(parent) => sessions(parent)
               }
             val resources = new Resources(name, parent_base)
 
@@ -142,7 +141,7 @@
                 sources = all_files.map(p => (p, SHA1.digest(p.file))),
                 session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base))
 
-            deps + (name -> base)
+            sessions + (name -> base)
           }
           catch {
             case ERROR(msg) =>
@@ -157,7 +156,7 @@
     val full_tree = load(options, dirs = dirs)
     val (_, tree) = full_tree.selection(sessions = List(session))
 
-    dependencies(global_theories = full_tree.global_theories, tree = tree)(session)
+    deps(tree, global_theories = full_tree.global_theories)(session)
   }
 
 
diff -r 68f8a0dab28b -r cc9e2f1f279d src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Apr 06 14:41:56 2017 +0200
+++ b/src/Pure/Tools/build.scala	Thu Apr 06 15:20:45 2017 +0200
@@ -395,9 +395,9 @@
     val full_tree = Sessions.load(build_options, dirs, select_dirs)
     val (selected, selected_tree) = selection(full_tree)
     val deps =
-      Sessions.dependencies(
-        progress, true, verbose, list_files, check_keywords,
-          full_tree.global_theories, selected_tree)
+      Sessions.deps(selected_tree, progress = progress, inlined_files = true,
+        verbose = verbose, list_files = list_files, check_keywords = check_keywords,
+        global_theories = full_tree.global_theories)
 
     def sources_stamp(name: String): List[String] =
       (selected_tree(name).meta_digest :: deps.sources(name)).map(_.toString).sorted