# HG changeset patch
# User wenzelm
# Date 1533134013 -7200
# Node ID c2dcb7f7a3ef4633f8d5ac0fceb077963bcb4bff
# Parent  0bc4919387800cc156a2ce02ee5d2577b4b604ea
tuned signature;

diff -r 0bc491938780 -r c2dcb7f7a3ef src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Jul 31 21:21:20 2018 +0200
+++ b/src/Pure/Tools/build.scala	Wed Aug 01 16:33:33 2018 +0200
@@ -64,15 +64,16 @@
       }
     }
 
-    def make_session_timing(sessions: Sessions.Structure, timing: Map[String, Double])
+    def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double])
       : Map[String, Double] =
     {
-      val maximals = sessions.build_graph.maximals.toSet
+      val maximals = sessions_structure.build_graph.maximals.toSet
       def desc_timing(name: String): Double =
       {
         if (maximals.contains(name)) timing(name)
         else {
-          val g = sessions.build_graph.restrict(sessions.build_descendants(List(name)).toSet)
+          val descendants = sessions_structure.build_descendants(List(name)).toSet
+          val g = sessions_structure.build_graph.restrict(descendants)
           (0.0 :: g.maximals.flatMap(desc => {
             val ps = g.all_preds(List(desc))
             if (ps.exists(p => timing.get(p).isEmpty)) None
@@ -83,16 +84,18 @@
       timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
     }
 
-    def apply(progress: Progress, sessions: Sessions.Structure, store: Sessions.Store): Queue =
+    def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store)
+      : Queue =
     {
-      val graph = sessions.build_graph
+      val graph = sessions_structure.build_graph
       val names = graph.keys
 
       val timings = names.map(name => (name, load_timings(progress, store, name)))
       val command_timings =
         timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
       val session_timing =
-        make_session_timing(sessions, timings.map({ case (name, (_, t)) => (name, t) }).toMap)
+        make_session_timing(sessions_structure,
+          timings.map({ case (name, (_, t)) => (name, t) }).toMap)
 
       object Ordering extends scala.math.Ordering[String]
       {
@@ -107,7 +110,7 @@
         def compare(name1: String, name2: String): Int =
           compare_timing(name2, name1) match {
             case 0 =>
-              sessions(name2).timeout compare sessions(name1).timeout match {
+              sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
                 case 0 => name1 compare name2
                 case ord => ord
               }