--- a/src/Pure/Admin/build_log.scala Tue May 02 11:05:04 2017 +0200
+++ b/src/Pure/Admin/build_log.scala Tue May 02 14:27:59 2017 +0200
@@ -899,4 +899,15 @@
Meta_Info.log_name(table1).sql + " = " + Meta_Info.log_name(table2).sql))
}
}
+
+
+ /* main operations */
+
+ def database_update(store: Store, db: SQL.Database, dirs: List[Path],
+ ml_statistics: Boolean = false, full_view: Boolean = false)
+ {
+ val files = Log_File.find_files(dirs)
+ store.write_info(db, files, ml_statistics = ml_statistics)
+ if (full_view) Build_Log.create_full_view(db)
+ }
}
--- a/src/Pure/Admin/isabelle_cronjob.scala Tue May 02 11:05:04 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Tue May 02 14:27:59 2017 +0200
@@ -148,14 +148,8 @@
def database_update(options: Options)
{
val store = Build_Log.store(options)
- val files = Build_Log.Log_File.find_files(database_dirs)
-
- // PostgreSQL server
using(store.open_database())(db =>
- {
- store.write_info(db, files, ml_statistics = true)
- Build_Log.create_full_view(db)
- })
+ Build_Log.database_update(store, db, database_dirs, ml_statistics = true, full_view = true))
}