src/Pure/Tools/build.scala
changeset 68731 c2dcb7f7a3ef
parent 68487 3d710aa23846
child 68734 c14a2cc9b5ef
equal deleted inserted replaced
68730:0bc491938780 68731:c2dcb7f7a3ef
    62           }
    62           }
    63           finally { db.close }
    63           finally { db.close }
    64       }
    64       }
    65     }
    65     }
    66 
    66 
    67     def make_session_timing(sessions: Sessions.Structure, timing: Map[String, Double])
    67     def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double])
    68       : Map[String, Double] =
    68       : Map[String, Double] =
    69     {
    69     {
    70       val maximals = sessions.build_graph.maximals.toSet
    70       val maximals = sessions_structure.build_graph.maximals.toSet
    71       def desc_timing(name: String): Double =
    71       def desc_timing(name: String): Double =
    72       {
    72       {
    73         if (maximals.contains(name)) timing(name)
    73         if (maximals.contains(name)) timing(name)
    74         else {
    74         else {
    75           val g = sessions.build_graph.restrict(sessions.build_descendants(List(name)).toSet)
    75           val descendants = sessions_structure.build_descendants(List(name)).toSet
       
    76           val g = sessions_structure.build_graph.restrict(descendants)
    76           (0.0 :: g.maximals.flatMap(desc => {
    77           (0.0 :: g.maximals.flatMap(desc => {
    77             val ps = g.all_preds(List(desc))
    78             val ps = g.all_preds(List(desc))
    78             if (ps.exists(p => timing.get(p).isEmpty)) None
    79             if (ps.exists(p => timing.get(p).isEmpty)) None
    79             else Some(ps.map(timing(_)).sum)
    80             else Some(ps.map(timing(_)).sum)
    80           })).max
    81           })).max
    81         }
    82         }
    82       }
    83       }
    83       timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
    84       timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
    84     }
    85     }
    85 
    86 
    86     def apply(progress: Progress, sessions: Sessions.Structure, store: Sessions.Store): Queue =
    87     def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store)
    87     {
    88       : Queue =
    88       val graph = sessions.build_graph
    89     {
       
    90       val graph = sessions_structure.build_graph
    89       val names = graph.keys
    91       val names = graph.keys
    90 
    92 
    91       val timings = names.map(name => (name, load_timings(progress, store, name)))
    93       val timings = names.map(name => (name, load_timings(progress, store, name)))
    92       val command_timings =
    94       val command_timings =
    93         timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
    95         timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
    94       val session_timing =
    96       val session_timing =
    95         make_session_timing(sessions, timings.map({ case (name, (_, t)) => (name, t) }).toMap)
    97         make_session_timing(sessions_structure,
       
    98           timings.map({ case (name, (_, t)) => (name, t) }).toMap)
    96 
    99 
    97       object Ordering extends scala.math.Ordering[String]
   100       object Ordering extends scala.math.Ordering[String]
    98       {
   101       {
    99         def compare_timing(name1: String, name2: String): Int =
   102         def compare_timing(name1: String, name2: String): Int =
   100         {
   103         {
   105         }
   108         }
   106 
   109 
   107         def compare(name1: String, name2: String): Int =
   110         def compare(name1: String, name2: String): Int =
   108           compare_timing(name2, name1) match {
   111           compare_timing(name2, name1) match {
   109             case 0 =>
   112             case 0 =>
   110               sessions(name2).timeout compare sessions(name1).timeout match {
   113               sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
   111                 case 0 => name1 compare name2
   114                 case 0 => name1 compare name2
   112                 case ord => ord
   115                 case ord => ord
   113               }
   116               }
   114             case ord => ord
   117             case ord => ord
   115           }
   118           }