src/Pure/Admin/isabelle_cronjob.scala
changeset 66865 c8b18abf23e1
parent 66864 5cb8ccc46e3e
child 66868 740d22146cb6
     1.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 14 21:50:12 2017 +0200
     1.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 14 22:05:22 2017 +0200
     1.3 @@ -131,17 +131,17 @@
     1.4      def profile: Build_Status.Profile =
     1.5        Build_Status.Profile(description, history, sql)
     1.6  
     1.7 -    def history_base_filter(hg: Mercurial.Repository): Set[String] =
     1.8 +    def history_base_filter(hg: Mercurial.Repository): Item => Boolean =
     1.9      {
    1.10        val rev0 = hg.id(history_base)
    1.11 -      val graph = hg.graph()
    1.12 -      (rev0 :: graph.all_succs(List(rev0))).toSet
    1.13 +      val nodes = hg.graph().all_succs(List(rev0)).toSet
    1.14 +      (item: Item) => nodes(item.isabelle_version)
    1.15      }
    1.16  
    1.17      def pick(
    1.18        options: Options,
    1.19        rev: String = "",
    1.20 -      filter: String => Boolean = (_: String) => true): Option[(String, Option[String])] =
    1.21 +      filter: Item => Boolean = _ => true): Option[(String, Option[String])] =
    1.22      {
    1.23        val afp_rev = if (afp) Some(Mercurial.repository(afp_repos).id()) else None
    1.24  
    1.25 @@ -150,9 +150,7 @@
    1.26        {
    1.27          def pick_days(days: Int, gap: Int): Option[(String, Option[String])] =
    1.28          {
    1.29 -          val items =
    1.30 -            recent_items(db, days, rev, afp_rev, sql).
    1.31 -              filter(item => filter(item.isabelle_version))
    1.32 +          val items = recent_items(db, days, rev, afp_rev, sql).filter(filter)
    1.33            def runs = unknown_runs(items).filter(run => run.length >= gap)
    1.34  
    1.35            if (historic || items.exists(_.known_versions(rev, afp_rev))) {