diff -r 0156222f2a18 -r a830c6257393 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Fri May 12 14:40:21 2017 +0200 +++ b/src/Pure/Admin/isabelle_cronjob.scala Fri May 12 16:11:59 2017 +0200 @@ -78,6 +78,27 @@ def unknown: Boolean = !known } + def recent_items(db: SQL.Database, days: Int, rev: String, sql: SQL.Source): List[Item] = + { + val select = + Build_Log.Data.select_recent_isabelle_versions(days = days, rev = rev, sql = "WHERE " + sql) + + db.using_statement(select)(stmt => + stmt.execute_query().iterator(res => + { + val known = res.bool(Build_Log.Data.known) + val isabelle_version = res.string(Build_Log.Prop.isabelle_version) + val pull_date = res.date(Build_Log.Data.pull_date) + Item(known, isabelle_version, pull_date) + }).toList) + } + + def unknown_runs(items: List[Item]): List[List[Item]] = + { + val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known)) + if (run.nonEmpty) run :: unknown_runs(rest) else Nil + } + sealed case class Remote_Build( description: String, host: String, @@ -102,32 +123,15 @@ val store = Build_Log.store(options) using(store.open_database())(db => { - val select = - Build_Log.Data.select_recent_isabelle_versions( - days = options.int("build_log_history") max history, rev = rev, sql = "WHERE " + sql) - - val recent_items = - db.using_statement(select)(stmt => - stmt.execute_query().iterator(res => - { - val known = res.bool(Build_Log.Data.known) - val isabelle_version = res.string(Build_Log.Prop.isabelle_version) - val pull_date = res.date(Build_Log.Data.pull_date) - Item(known, isabelle_version, pull_date) - }).toList) - - def unknown_runs(items: List[Item]): List[List[Item]] = - { - val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known)) - if (run.nonEmpty) run :: unknown_runs(rest) else Nil - } + val days = options.int("build_log_history") max history + val items = recent_items(db, days = days, rev = rev, sql = sql) val known_rev = - rev != "" && recent_items.exists(item => item.known && item.isabelle_version == rev) + rev != "" && items.exists(item => item.known && item.isabelle_version == rev) if (history > 0 || known_rev) { val longest_run = - (List.empty[Item] /: unknown_runs(recent_items))({ case (item1, item2) => + (List.empty[Item] /: unknown_runs(items))({ case (item1, item2) => if (item1.length >= item2.length) item1 else item2 }) if (longest_run.isEmpty) None