# HG changeset patch
# User wenzelm
# Date 1529756633 -7200
# Node ID 6984a55f3cbac0efe49e56ab470a3c0679b0d5c8
# Parent  28f9e9b80c49f6159571891780a17ec98025d422
clarified queue ordering: take session descendants into account, notably for "slow" AFP sessions;

diff -r 28f9e9b80c49 -r 6984a55f3cba src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Jun 22 21:55:20 2018 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jun 23 14:23:53 2018 +0200
@@ -64,6 +64,21 @@
       }
     }
 
+    def make_session_timing(sessions: Sessions.Structure, timing: Map[String, Double])
+      : Map[String, Double] =
+    {
+      def desc_timing(name: String): Double =
+      {
+        val g = sessions.build_graph.restrict(sessions.build_descendants(List(name)).toSet)
+        (0.0 :: g.maximals.flatMap(desc => {
+          val ps = g.all_preds(List(desc))
+          if (ps.exists(p => timing.get(p).isEmpty)) None
+          else Some(ps.map(timing(_)).sum)
+        })).max
+      }
+      timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
+    }
+
     def apply(progress: Progress, sessions: Sessions.Structure, store: Sessions.Store): Queue =
     {
       val graph = sessions.build_graph
@@ -71,11 +86,9 @@
 
       val timings = names.map(name => (name, load_timings(progress, store, name)))
       val command_timings =
-        Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
+        timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
       val session_timing =
-        Map(timings.map({ case (name, (_, t)) => (name, t) }): _*).withDefaultValue(0.0)
-
-      def outdegree(name: String): Int = graph.imm_succs(name).size
+        make_session_timing(sessions, timings.map({ case (name, (_, t)) => (name, t) }).toMap)
 
       object Ordering extends scala.math.Ordering[String]
       {
@@ -88,14 +101,10 @@
         }
 
         def compare(name1: String, name2: String): Int =
-          outdegree(name2) compare outdegree(name1) match {
+          compare_timing(name2, name1) match {
             case 0 =>
-              compare_timing(name2, name1) match {
-                case 0 =>
-                  sessions(name2).timeout compare sessions(name1).timeout match {
-                    case 0 => name1 compare name2
-                    case ord => ord
-                  }
+              sessions(name2).timeout compare sessions(name1).timeout match {
+                case 0 => name1 compare name2
                 case ord => ord
               }
             case ord => ord