src/Pure/Admin/isabelle_cronjob.scala
changeset 66880 486f4af28db9
parent 66879 593053cac3be
child 66883 ee874941dfb8
     1.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Wed Oct 18 11:53:01 2017 +0200
     1.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Wed Oct 18 19:53:19 2017 +0200
     1.3 @@ -86,6 +86,7 @@
     1.4    def recent_items(db: SQL.Database,
     1.5      days: Int, rev: String, afp_rev: Option[String], sql: SQL.Source): List[Item] =
     1.6    {
     1.7 +    val afp = afp_rev.isDefined
     1.8      val select =
     1.9        Build_Log.Data.select_recent_versions(
    1.10          days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql)
    1.11 @@ -95,10 +96,8 @@
    1.12        {
    1.13          val known = res.bool(Build_Log.Data.known)
    1.14          val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
    1.15 -        val afp_version =
    1.16 -          if (afp_rev.isEmpty) None
    1.17 -          else proper_string(res.string(Build_Log.Prop.afp_version))
    1.18 -        val pull_date = res.date(Build_Log.Data.pull_date)
    1.19 +        val afp_version = if (afp) proper_string(res.string(Build_Log.Prop.afp_version)) else None
    1.20 +        val pull_date = res.date(Build_Log.Data.pull_date(afp))
    1.21          Item(known, isabelle_version, afp_version, pull_date)
    1.22        }).toList)
    1.23    }
    1.24 @@ -129,7 +128,7 @@
    1.25        (if (detect == "") "" else " AND " + SQL.enclose(detect))
    1.26  
    1.27      def profile: Build_Status.Profile =
    1.28 -      Build_Status.Profile(description, history, sql)
    1.29 +      Build_Status.Profile(description, history = history, afp = afp, sql = sql)
    1.30  
    1.31      def history_base_filter(hg: Mercurial.Repository): Item => Boolean =
    1.32      {