# HG changeset patch
# User wenzelm
# Date 1494599573 -7200
# Node ID 356c2b488cf30bc872a2b5615e14b59b74e04d78
# Parent  8d5ac49388ea9e5c747de6a5c75b415ba43e7591
explore older history;

diff -r 8d5ac49388ea -r 356c2b488cf3 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Fri May 12 16:24:29 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri May 12 16:32:53 2017 +0200
@@ -124,23 +124,29 @@
       val store = Build_Log.store(options)
       using(store.open_database())(db =>
       {
-        val days = options.int("build_log_history") max history
-        val items = recent_items(db, days = days, rev = rev, sql = sql)
-        def runs = unknown_runs(items)
+        def pick_days(days: Int): Option[String] =
+        {
+          val items = recent_items(db, days = days, rev = rev, sql = sql)
+          def runs = unknown_runs(items)
 
-        val known_rev =
-          rev != "" && items.exists(item => item.known && item.isabelle_version == rev)
+          val known_rev =
+            rev != "" && items.exists(item => item.known && item.isabelle_version == rev)
 
-        if (historic || known_rev) {
-          val longest_run =
-            (List.empty[Item] /: runs)({ case (item1, item2) =>
-              if (item1.length >= item2.length) item1 else item2
-            })
-          if (longest_run.isEmpty) None
-          else Some(longest_run(longest_run.length / 2).isabelle_version)
+          if (historic || known_rev) {
+            val longest_run =
+              (List.empty[Item] /: runs)({ case (item1, item2) =>
+                if (item1.length >= item2.length) item1 else item2
+              })
+            if (longest_run.isEmpty) None
+            else Some(longest_run(longest_run.length / 2).isabelle_version)
+          }
+          else if (rev != "") Some(rev)
+          else runs.flatten.headOption.map(_.isabelle_version)
         }
-        else if (rev != "") Some(rev)
-        else runs.flatten.headOption.map(_.isabelle_version)
+
+        pick_days(options.int("build_log_history") max history) orElse
+        pick_days(100) orElse
+        pick_days(1000)
       })
     }
   }