tuned;
authorwenzelm
Sat Jun 23 17:05:59 2018 +0200 (13 months ago)
changeset 684873d710aa23846
parent 68486 6984a55f3cba
child 68489 56034bd1b5f6
tuned;
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.scala	Sat Jun 23 14:23:53 2018 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Sat Jun 23 17:05:59 2018 +0200
     1.3 @@ -67,14 +67,18 @@
     1.4      def make_session_timing(sessions: Sessions.Structure, timing: Map[String, Double])
     1.5        : Map[String, Double] =
     1.6      {
     1.7 +      val maximals = sessions.build_graph.maximals.toSet
     1.8        def desc_timing(name: String): Double =
     1.9        {
    1.10 -        val g = sessions.build_graph.restrict(sessions.build_descendants(List(name)).toSet)
    1.11 -        (0.0 :: g.maximals.flatMap(desc => {
    1.12 -          val ps = g.all_preds(List(desc))
    1.13 -          if (ps.exists(p => timing.get(p).isEmpty)) None
    1.14 -          else Some(ps.map(timing(_)).sum)
    1.15 -        })).max
    1.16 +        if (maximals.contains(name)) timing(name)
    1.17 +        else {
    1.18 +          val g = sessions.build_graph.restrict(sessions.build_descendants(List(name)).toSet)
    1.19 +          (0.0 :: g.maximals.flatMap(desc => {
    1.20 +            val ps = g.all_preds(List(desc))
    1.21 +            if (ps.exists(p => timing.get(p).isEmpty)) None
    1.22 +            else Some(ps.map(timing(_)).sum)
    1.23 +          })).max
    1.24 +        }
    1.25        }
    1.26        timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
    1.27      }