# HG changeset patch
# User wenzelm
# Date 1676146920 -3600
# Node ID b3700ee8b0ad3ef04f257d2341556be80d32f4b9
# Parent  6ed94a0ec7237cfacebfae5838b7cd48ff3ce434
tuned;

diff -r 6ed94a0ec723 -r b3700ee8b0ad src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sat Feb 11 21:13:28 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sat Feb 11 21:22:00 2023 +0100
@@ -72,30 +72,29 @@
           for (name <- build_graph.keys_iterator)
           yield name -> Build_Process.Session_Context(name, store, progress = progress))
 
-      val maximals = build_graph.maximals.toSet
-
-      def descendants_time(name: String): Double = {
-        if (maximals.contains(name)) sessions(name).old_time.seconds
-        else {
-          val descendants = build_graph.all_succs(List(name)).toSet
-          val g = build_graph.restrict(descendants)
-          (0.0 :: g.maximals.flatMap { desc =>
-            val ps = g.all_preds(List(desc))
-            if (ps.exists(p => !sessions.isDefinedAt(p))) None
-            else Some(ps.map(p => sessions(p).old_time.seconds).sum)
-          }).max
+      val sessions_time = {
+        val maximals = build_graph.maximals.toSet
+        def descendants_time(name: String): Double = {
+          if (maximals.contains(name)) sessions(name).old_time.seconds
+          else {
+            val descendants = build_graph.all_succs(List(name)).toSet
+            val g = build_graph.restrict(descendants)
+            (0.0 :: g.maximals.flatMap { desc =>
+              val ps = g.all_preds(List(desc))
+              if (ps.exists(p => !sessions.isDefinedAt(p))) None
+              else Some(ps.map(p => sessions(p).old_time.seconds).sum)
+            }).max
+          }
         }
+        Map.from(
+          for (name <- sessions.keysIterator)
+          yield name -> descendants_time(name)).withDefaultValue(0.0)
       }
 
-      val session_time =
-        Map.from(
-          for ((name, context) <- sessions.iterator)
-          yield name -> descendants_time(name)).withDefaultValue(0.0)
-
       val ordering =
         new Ordering[String] {
           def compare(name1: String, name2: String): Int =
-            session_time(name2) compare session_time(name1) match {
+            sessions_time(name2) compare sessions_time(name1) match {
               case 0 =>
                 sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
                   case 0 => name1 compare name2