123 val store = Build_Log.store(options) |
123 val store = Build_Log.store(options) |
124 using(store.open_database())(db => |
124 using(store.open_database())(db => |
125 { |
125 { |
126 val days = options.int("build_log_history") max history |
126 val days = options.int("build_log_history") max history |
127 val items = recent_items(db, days = days, rev = rev, sql = sql) |
127 val items = recent_items(db, days = days, rev = rev, sql = sql) |
|
128 def runs = unknown_runs(items) |
128 |
129 |
129 val known_rev = |
130 val known_rev = |
130 rev != "" && items.exists(item => item.known && item.isabelle_version == rev) |
131 rev != "" && items.exists(item => item.known && item.isabelle_version == rev) |
131 |
132 |
132 if (history > 0 || known_rev) { |
133 if (history > 0 || known_rev) { |
133 val longest_run = |
134 val longest_run = |
134 (List.empty[Item] /: unknown_runs(items))({ case (item1, item2) => |
135 (List.empty[Item] /: runs)({ case (item1, item2) => |
135 if (item1.length >= item2.length) item1 else item2 |
136 if (item1.length >= item2.length) item1 else item2 |
136 }) |
137 }) |
137 if (longest_run.isEmpty) None |
138 if (longest_run.isEmpty) None |
138 else Some(longest_run(longest_run.length / 2).isabelle_version) |
139 else Some(longest_run(longest_run.length / 2).isabelle_version) |
139 } |
140 } |
140 else Some(rev) |
141 else if (rev != "") Some(rev) |
|
142 else runs.flatten.headOption.map(_.isabelle_version) |
141 }) |
143 }) |
142 } |
144 } |
143 } |
145 } |
144 |
146 |
145 val remote_builds_old: List[Remote_Build] = |
147 val remote_builds_old: List[Remote_Build] = |