tuned -- more open to experimentation;
authorwenzelm
Fri May 12 16:11:59 2017 +0200 (2017-05-12)
changeset 65807a830c6257393
parent 65806 0156222f2a18
child 65808 cb3e9d7f1d5f
tuned -- more open to experimentation;
src/Pure/Admin/isabelle_cronjob.scala
     1.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Fri May 12 14:40:21 2017 +0200
     1.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri May 12 16:11:59 2017 +0200
     1.3 @@ -78,6 +78,27 @@
     1.4      def unknown: Boolean = !known
     1.5    }
     1.6  
     1.7 +  def recent_items(db: SQL.Database, days: Int, rev: String, sql: SQL.Source): List[Item] =
     1.8 +  {
     1.9 +    val select =
    1.10 +      Build_Log.Data.select_recent_isabelle_versions(days = days, rev = rev, sql = "WHERE " + sql)
    1.11 +
    1.12 +    db.using_statement(select)(stmt =>
    1.13 +      stmt.execute_query().iterator(res =>
    1.14 +      {
    1.15 +        val known = res.bool(Build_Log.Data.known)
    1.16 +        val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
    1.17 +        val pull_date = res.date(Build_Log.Data.pull_date)
    1.18 +        Item(known, isabelle_version, pull_date)
    1.19 +      }).toList)
    1.20 +  }
    1.21 +
    1.22 +  def unknown_runs(items: List[Item]): List[List[Item]] =
    1.23 +  {
    1.24 +    val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known))
    1.25 +    if (run.nonEmpty) run :: unknown_runs(rest) else Nil
    1.26 +  }
    1.27 +
    1.28    sealed case class Remote_Build(
    1.29      description: String,
    1.30      host: String,
    1.31 @@ -102,32 +123,15 @@
    1.32        val store = Build_Log.store(options)
    1.33        using(store.open_database())(db =>
    1.34        {
    1.35 -        val select =
    1.36 -          Build_Log.Data.select_recent_isabelle_versions(
    1.37 -            days = options.int("build_log_history") max history, rev = rev, sql = "WHERE " + sql)
    1.38 -
    1.39 -        val recent_items =
    1.40 -          db.using_statement(select)(stmt =>
    1.41 -            stmt.execute_query().iterator(res =>
    1.42 -            {
    1.43 -              val known = res.bool(Build_Log.Data.known)
    1.44 -              val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
    1.45 -              val pull_date = res.date(Build_Log.Data.pull_date)
    1.46 -              Item(known, isabelle_version, pull_date)
    1.47 -            }).toList)
    1.48 -
    1.49 -        def unknown_runs(items: List[Item]): List[List[Item]] =
    1.50 -        {
    1.51 -          val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known))
    1.52 -          if (run.nonEmpty) run :: unknown_runs(rest) else Nil
    1.53 -        }
    1.54 +        val days = options.int("build_log_history") max history
    1.55 +        val items = recent_items(db, days = days, rev = rev, sql = sql)
    1.56  
    1.57          val known_rev =
    1.58 -          rev != "" && recent_items.exists(item => item.known && item.isabelle_version == rev)
    1.59 +          rev != "" && items.exists(item => item.known && item.isabelle_version == rev)
    1.60  
    1.61          if (history > 0 || known_rev) {
    1.62            val longest_run =
    1.63 -            (List.empty[Item] /: unknown_runs(recent_items))({ case (item1, item2) =>
    1.64 +            (List.empty[Item] /: unknown_runs(items))({ case (item1, item2) =>
    1.65                if (item1.length >= item2.length) item1 else item2
    1.66              })
    1.67            if (longest_run.isEmpty) None