src/Pure/Tools/build.scala
changeset 68731 c2dcb7f7a3ef
parent 68487 3d710aa23846
child 68734 c14a2cc9b5ef
     1.1 --- a/src/Pure/Tools/build.scala	Tue Jul 31 21:21:20 2018 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Aug 01 16:33:33 2018 +0200
     1.3 @@ -64,15 +64,16 @@
     1.4        }
     1.5      }
     1.6  
     1.7 -    def make_session_timing(sessions: Sessions.Structure, timing: Map[String, Double])
     1.8 +    def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double])
     1.9        : Map[String, Double] =
    1.10      {
    1.11 -      val maximals = sessions.build_graph.maximals.toSet
    1.12 +      val maximals = sessions_structure.build_graph.maximals.toSet
    1.13        def desc_timing(name: String): Double =
    1.14        {
    1.15          if (maximals.contains(name)) timing(name)
    1.16          else {
    1.17 -          val g = sessions.build_graph.restrict(sessions.build_descendants(List(name)).toSet)
    1.18 +          val descendants = sessions_structure.build_descendants(List(name)).toSet
    1.19 +          val g = sessions_structure.build_graph.restrict(descendants)
    1.20            (0.0 :: g.maximals.flatMap(desc => {
    1.21              val ps = g.all_preds(List(desc))
    1.22              if (ps.exists(p => timing.get(p).isEmpty)) None
    1.23 @@ -83,16 +84,18 @@
    1.24        timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
    1.25      }
    1.26  
    1.27 -    def apply(progress: Progress, sessions: Sessions.Structure, store: Sessions.Store): Queue =
    1.28 +    def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store)
    1.29 +      : Queue =
    1.30      {
    1.31 -      val graph = sessions.build_graph
    1.32 +      val graph = sessions_structure.build_graph
    1.33        val names = graph.keys
    1.34  
    1.35        val timings = names.map(name => (name, load_timings(progress, store, name)))
    1.36        val command_timings =
    1.37          timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
    1.38        val session_timing =
    1.39 -        make_session_timing(sessions, timings.map({ case (name, (_, t)) => (name, t) }).toMap)
    1.40 +        make_session_timing(sessions_structure,
    1.41 +          timings.map({ case (name, (_, t)) => (name, t) }).toMap)
    1.42  
    1.43        object Ordering extends scala.math.Ordering[String]
    1.44        {
    1.45 @@ -107,7 +110,7 @@
    1.46          def compare(name1: String, name2: String): Int =
    1.47            compare_timing(name2, name1) match {
    1.48              case 0 =>
    1.49 -              sessions(name2).timeout compare sessions(name1).timeout match {
    1.50 +              sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
    1.51                  case 0 => name1 compare name2
    1.52                  case ord => ord
    1.53                }