src/Pure/Tools/build.scala
changeset 68486 6984a55f3cba
parent 68331 7eaaa8f48331
child 68487 3d710aa23846
     1.1 --- a/src/Pure/Tools/build.scala	Fri Jun 22 21:55:20 2018 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Sat Jun 23 14:23:53 2018 +0200
     1.3 @@ -64,6 +64,21 @@
     1.4        }
     1.5      }
     1.6  
     1.7 +    def make_session_timing(sessions: Sessions.Structure, timing: Map[String, Double])
     1.8 +      : Map[String, Double] =
     1.9 +    {
    1.10 +      def desc_timing(name: String): Double =
    1.11 +      {
    1.12 +        val g = sessions.build_graph.restrict(sessions.build_descendants(List(name)).toSet)
    1.13 +        (0.0 :: g.maximals.flatMap(desc => {
    1.14 +          val ps = g.all_preds(List(desc))
    1.15 +          if (ps.exists(p => timing.get(p).isEmpty)) None
    1.16 +          else Some(ps.map(timing(_)).sum)
    1.17 +        })).max
    1.18 +      }
    1.19 +      timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
    1.20 +    }
    1.21 +
    1.22      def apply(progress: Progress, sessions: Sessions.Structure, store: Sessions.Store): Queue =
    1.23      {
    1.24        val graph = sessions.build_graph
    1.25 @@ -71,11 +86,9 @@
    1.26  
    1.27        val timings = names.map(name => (name, load_timings(progress, store, name)))
    1.28        val command_timings =
    1.29 -        Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
    1.30 +        timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
    1.31        val session_timing =
    1.32 -        Map(timings.map({ case (name, (_, t)) => (name, t) }): _*).withDefaultValue(0.0)
    1.33 -
    1.34 -      def outdegree(name: String): Int = graph.imm_succs(name).size
    1.35 +        make_session_timing(sessions, timings.map({ case (name, (_, t)) => (name, t) }).toMap)
    1.36  
    1.37        object Ordering extends scala.math.Ordering[String]
    1.38        {
    1.39 @@ -88,14 +101,10 @@
    1.40          }
    1.41  
    1.42          def compare(name1: String, name2: String): Int =
    1.43 -          outdegree(name2) compare outdegree(name1) match {
    1.44 +          compare_timing(name2, name1) match {
    1.45              case 0 =>
    1.46 -              compare_timing(name2, name1) match {
    1.47 -                case 0 =>
    1.48 -                  sessions(name2).timeout compare sessions(name1).timeout match {
    1.49 -                    case 0 => name1 compare name2
    1.50 -                    case ord => ord
    1.51 -                  }
    1.52 +              sessions(name2).timeout compare sessions(name1).timeout match {
    1.53 +                case 0 => name1 compare name2
    1.54                  case ord => ord
    1.55                }
    1.56              case ord => ord