# HG changeset patch
# User wenzelm
# Date 1493728079 -7200
# Node ID 3722be87305c507878fd50fccd130452459d9418
# Parent  45632d594bdb912e02ee62250a58025b3ef6f396
tuned signature;

diff -r 45632d594bdb -r 3722be87305c src/Pure/Admin/build_log.scala
--- 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)
+  }
 }
diff -r 45632d594bdb -r 3722be87305c src/Pure/Admin/isabelle_cronjob.scala
--- 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))
   }