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 { |