src/Pure/Admin/isabelle_cronjob.scala
changeset 65810 356c2b488cf3
parent 65809 8d5ac49388ea
child 65820 a5d4958d0901
     1.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Fri May 12 16:24:29 2017 +0200
     1.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri May 12 16:32:53 2017 +0200
     1.3 @@ -124,23 +124,29 @@
     1.4        val store = Build_Log.store(options)
     1.5        using(store.open_database())(db =>
     1.6        {
     1.7 -        val days = options.int("build_log_history") max history
     1.8 -        val items = recent_items(db, days = days, rev = rev, sql = sql)
     1.9 -        def runs = unknown_runs(items)
    1.10 +        def pick_days(days: Int): Option[String] =
    1.11 +        {
    1.12 +          val items = recent_items(db, days = days, rev = rev, sql = sql)
    1.13 +          def runs = unknown_runs(items)
    1.14  
    1.15 -        val known_rev =
    1.16 -          rev != "" && items.exists(item => item.known && item.isabelle_version == rev)
    1.17 +          val known_rev =
    1.18 +            rev != "" && items.exists(item => item.known && item.isabelle_version == rev)
    1.19  
    1.20 -        if (historic || known_rev) {
    1.21 -          val longest_run =
    1.22 -            (List.empty[Item] /: runs)({ case (item1, item2) =>
    1.23 -              if (item1.length >= item2.length) item1 else item2
    1.24 -            })
    1.25 -          if (longest_run.isEmpty) None
    1.26 -          else Some(longest_run(longest_run.length / 2).isabelle_version)
    1.27 +          if (historic || known_rev) {
    1.28 +            val longest_run =
    1.29 +              (List.empty[Item] /: runs)({ case (item1, item2) =>
    1.30 +                if (item1.length >= item2.length) item1 else item2
    1.31 +              })
    1.32 +            if (longest_run.isEmpty) None
    1.33 +            else Some(longest_run(longest_run.length / 2).isabelle_version)
    1.34 +          }
    1.35 +          else if (rev != "") Some(rev)
    1.36 +          else runs.flatten.headOption.map(_.isabelle_version)
    1.37          }
    1.38 -        else if (rev != "") Some(rev)
    1.39 -        else runs.flatten.headOption.map(_.isabelle_version)
    1.40 +
    1.41 +        pick_days(options.int("build_log_history") max history) orElse
    1.42 +        pick_days(100) orElse
    1.43 +        pick_days(1000)
    1.44        })
    1.45      }
    1.46    }