# HG changeset patch
# User wenzelm
# Date 1494257626 -7200
# Node ID a42c9e375405c36802bd272fc4a2b023c8d51257
# Parent  666a1bac126ba19aa2640dd179e3bc093581483e
tuned -- inlined single use;

diff -r 666a1bac126b -r a42c9e375405 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon May 08 17:16:40 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Mon May 08 17:33:46 2017 +0200
@@ -686,9 +686,6 @@
         " GROUP BY " + version)
     }
 
-
-    /* recent pull_date entries */
-
     def recent_time(days: Int): SQL.Source =
       "now() - INTERVAL '" + days.max(0) + " days'"
 
@@ -699,14 +696,6 @@
         table.select(table.columns, "WHERE " + pull_date(table) + " > " + recent_time(days)))
     }
 
-    def recent_pull_date_select(table1: SQL.Table, columns: List[SQL.Column], days: Int,
-      distinct: Boolean = false): SQL.Source =
-    {
-      val table2 = recent_pull_date_table(days)
-      table1.select(columns, distinct = distinct) + SQL.join_inner + table2.query_named +
-      " ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2)
-    }
-
 
     /* universal view on main data */
 
@@ -770,6 +759,14 @@
       Isabelle_System.mkdirs(sqlite_database.dir)
       sqlite_database.file.delete
 
+      val select_recent_log_names =
+      {
+        val table1 = Data.meta_info_table
+        val table2 = Data.recent_pull_date_table(days)
+        table1.select(List(Data.log_name), distinct = true) + SQL.join_inner + table2.query_named +
+          " ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2)
+      }
+
       using(SQLite.open_database(sqlite_database))(db2 =>
       {
         db.transaction {
@@ -780,10 +777,8 @@
             db2.create_table(Data.ml_statistics_table)
 
             val recent_log_names =
-              db.using_statement(
-                Data.recent_pull_date_select(
-                  Data.meta_info_table, List(Data.log_name), days, distinct = true))(stmt =>
-                    stmt.execute_query().iterator(_.string(Data.log_name)).toList)
+              db.using_statement(select_recent_log_names)(stmt =>
+                stmt.execute_query().iterator(_.string(Data.log_name)).toList)
 
             for (log_name <- recent_log_names) {
               read_meta_info(db, log_name).foreach(meta_info =>