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