84 } |
84 } |
85 |
85 |
86 def recent_items(db: SQL.Database, |
86 def recent_items(db: SQL.Database, |
87 days: Int, rev: String, afp_rev: Option[String], sql: SQL.Source): List[Item] = |
87 days: Int, rev: String, afp_rev: Option[String], sql: SQL.Source): List[Item] = |
88 { |
88 { |
|
89 val afp = afp_rev.isDefined |
89 val select = |
90 val select = |
90 Build_Log.Data.select_recent_versions( |
91 Build_Log.Data.select_recent_versions( |
91 days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql) |
92 days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql) |
92 |
93 |
93 db.using_statement(select)(stmt => |
94 db.using_statement(select)(stmt => |
94 stmt.execute_query().iterator(res => |
95 stmt.execute_query().iterator(res => |
95 { |
96 { |
96 val known = res.bool(Build_Log.Data.known) |
97 val known = res.bool(Build_Log.Data.known) |
97 val isabelle_version = res.string(Build_Log.Prop.isabelle_version) |
98 val isabelle_version = res.string(Build_Log.Prop.isabelle_version) |
98 val afp_version = |
99 val afp_version = if (afp) proper_string(res.string(Build_Log.Prop.afp_version)) else None |
99 if (afp_rev.isEmpty) None |
100 val pull_date = res.date(Build_Log.Data.pull_date(afp)) |
100 else proper_string(res.string(Build_Log.Prop.afp_version)) |
|
101 val pull_date = res.date(Build_Log.Data.pull_date) |
|
102 Item(known, isabelle_version, afp_version, pull_date) |
101 Item(known, isabelle_version, afp_version, pull_date) |
103 }).toList) |
102 }).toList) |
104 } |
103 } |
105 |
104 |
106 def unknown_runs(items: List[Item]): List[List[Item]] = |
105 def unknown_runs(items: List[Item]): List[List[Item]] = |
127 Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " + |
126 Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " + |
128 Build_Log.Prop.build_host + " = " + SQL.string(host) + |
127 Build_Log.Prop.build_host + " = " + SQL.string(host) + |
129 (if (detect == "") "" else " AND " + SQL.enclose(detect)) |
128 (if (detect == "") "" else " AND " + SQL.enclose(detect)) |
130 |
129 |
131 def profile: Build_Status.Profile = |
130 def profile: Build_Status.Profile = |
132 Build_Status.Profile(description, history, sql) |
131 Build_Status.Profile(description, history = history, afp = afp, sql = sql) |
133 |
132 |
134 def history_base_filter(hg: Mercurial.Repository): Item => Boolean = |
133 def history_base_filter(hg: Mercurial.Repository): Item => Boolean = |
135 { |
134 { |
136 val rev0 = hg.id(history_base) |
135 val rev0 = hg.id(history_base) |
137 val nodes = hg.graph().all_succs(List(rev0)).toSet |
136 val nodes = hg.graph().all_succs(List(rev0)).toSet |