58 |
58 |
59 override def toString: String = session |
59 override def toString: String = session |
60 } |
60 } |
61 |
61 |
62 object Context { |
62 object Context { |
63 private def make_session_timing( |
|
64 sessions_structure: Sessions.Structure, |
|
65 timing: Map[String, Double] |
|
66 ) : Map[String, Double] = { |
|
67 val maximals = sessions_structure.build_graph.maximals.toSet |
|
68 def desc_timing(session_name: String): Double = { |
|
69 if (maximals.contains(session_name)) timing(session_name) |
|
70 else { |
|
71 val descendants = sessions_structure.build_descendants(List(session_name)).toSet |
|
72 val g = sessions_structure.build_graph.restrict(descendants) |
|
73 (0.0 :: g.maximals.flatMap { desc => |
|
74 val ps = g.all_preds(List(desc)) |
|
75 if (ps.exists(p => !timing.isDefinedAt(p))) None |
|
76 else Some(ps.map(timing(_)).sum) |
|
77 }).max |
|
78 } |
|
79 } |
|
80 timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0) |
|
81 } |
|
82 |
|
83 def apply( |
63 def apply( |
84 sessions_structure: Sessions.Structure, |
64 sessions_structure: Sessions.Structure, |
85 store: Sessions.Store, |
65 store: Sessions.Store, |
86 progress: Progress = new Progress |
66 progress: Progress = new Progress |
87 ): Context = { |
67 ): Context = { |
|
68 val build_graph = sessions_structure.build_graph |
|
69 |
88 val sessions = |
70 val sessions = |
89 Map.from( |
71 Map.from( |
90 for (session <- sessions_structure.build_graph.keys_iterator) |
72 for (name <- build_graph.keys_iterator) |
91 yield session -> Build_Process.Session_Context(session, store, progress = progress)) |
73 yield name -> Build_Process.Session_Context(name, store, progress = progress)) |
92 |
74 |
93 val session_timing = |
75 val maximals = build_graph.maximals.toSet |
94 make_session_timing(sessions_structure, |
76 |
95 Map.from(for ((name, context) <- sessions.iterator) yield name -> context.old_time.seconds)) |
77 def descendants_time(name: String): Double = { |
|
78 if (maximals.contains(name)) sessions(name).old_time.seconds |
|
79 else { |
|
80 val descendants = build_graph.all_succs(List(name)).toSet |
|
81 val g = build_graph.restrict(descendants) |
|
82 (0.0 :: g.maximals.flatMap { desc => |
|
83 val ps = g.all_preds(List(desc)) |
|
84 if (ps.exists(p => !sessions.isDefinedAt(p))) None |
|
85 else Some(ps.map(p => sessions(p).old_time.seconds).sum) |
|
86 }).max |
|
87 } |
|
88 } |
|
89 |
|
90 val session_time = |
|
91 Map.from( |
|
92 for ((name, context) <- sessions.iterator) |
|
93 yield name -> descendants_time(name)).withDefaultValue(0.0) |
96 |
94 |
97 val ordering = |
95 val ordering = |
98 new Ordering[String] { |
96 new Ordering[String] { |
99 def compare(name1: String, name2: String): Int = |
97 def compare(name1: String, name2: String): Int = |
100 session_timing(name2) compare session_timing(name1) match { |
98 session_time(name2) compare session_time(name1) match { |
101 case 0 => |
99 case 0 => |
102 sessions_structure(name2).timeout compare sessions_structure(name1).timeout match { |
100 sessions_structure(name2).timeout compare sessions_structure(name1).timeout match { |
103 case 0 => name1 compare name2 |
101 case 0 => name1 compare name2 |
104 case ord => ord |
102 case ord => ord |
105 } |
103 } |