# HG changeset patch
# User wenzelm
# Date 1493754123 -7200
# Node ID c1eab527bfa7cf667efa47f54645ea4dacc93443
# Parent  2181b5615c64663c7d5ffb37445e36d82ffce9d6
tuned signature;

diff -r 2181b5615c64 -r c1eab527bfa7 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue May 02 21:38:23 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Tue May 02 21:42:03 2017 +0200
@@ -890,35 +890,40 @@
   }
 
 
-  /* full view on build_log data */
+  /** high-level database structure **/
 
-  // WARNING: This may cause performance problems, e.g. with sqlitebrowser
+  object Database
+  {
+    /* full view on build_log data */
 
-  val full_view: SQL.View =
-    SQL.View("isabelle_build_log",
-      Meta_Info.table.columns :::
-        Build_Info.sessions_table.columns.tail.map(_.copy(primary_key = false)))
+    // WARNING: This may cause performance problems, e.g. with sqlitebrowser
+
+    val full_view: SQL.View =
+      SQL.View("isabelle_build_log",
+        Meta_Info.table.columns :::
+          Build_Info.sessions_table.columns.tail.map(_.copy(primary_key = false)))
 
-  def create_full_view(db: SQL.Database)
-  {
-    if (!db.tables.contains(full_view.name)) {
-      val table1 = Meta_Info.table
-      val table2 = Build_Info.sessions_table
-      db.create_view(full_view,
-        SQL.select(Meta_Info.log_name(table1) :: full_view.columns.tail) +
-        SQL.join(table1, table2,
-          Meta_Info.log_name(table1).sql + " = " + Meta_Info.log_name(table2).sql))
+    def create_full_view(db: SQL.Database)
+    {
+      if (!db.tables.contains(full_view.name)) {
+        val table1 = Meta_Info.table
+        val table2 = Build_Info.sessions_table
+        db.create_view(full_view,
+          SQL.select(Meta_Info.log_name(table1) :: full_view.columns.tail) +
+          SQL.join(table1, table2,
+            Meta_Info.log_name(table1).sql + " = " + Meta_Info.log_name(table2).sql))
+      }
+    }
+
+
+    /* main operations */
+
+    def 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) create_full_view(db)
     }
   }
-
-
-  /* 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 2181b5615c64 -r c1eab527bfa7 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue May 02 21:38:23 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue May 02 21:42:03 2017 +0200
@@ -149,7 +149,7 @@
   {
     val store = Build_Log.store(options)
     using(store.open_database())(db =>
-      Build_Log.database_update(store, db, database_dirs, ml_statistics = true, full_view = true))
+      Build_Log.Database.update(store, db, database_dirs, ml_statistics = true, full_view = true))
   }