src/Pure/Admin/build_log.scala

--- a/src/Pure/Admin/build_log.scala	Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_log.scala	Mon Mar 01 22:22:12 2021 +0100
@@ -874,7 +874,8 @@
         ssh_close = true)
     }
 
-    def update_database(db: PostgreSQL.Database, dirs: List[Path], ml_statistics: Boolean = false)
+    def update_database(
+      db: PostgreSQL.Database, dirs: List[Path], ml_statistics: Boolean = false): Unit =
     {
       val log_files =
         dirs.flatMap(dir =>
@@ -887,7 +888,7 @@
     }
 
     def snapshot_database(db: PostgreSQL.Database, sqlite_database: Path,
-      days: Int = 100, ml_statistics: Boolean = false)
+      days: Int = 100, ml_statistics: Boolean = false): Unit =
     {
       Isabelle_System.make_directory(sqlite_database.dir)
       sqlite_database.file.delete
@@ -952,7 +953,7 @@
       db.using_statement(table.select(List(column), distinct = true))(stmt =>
         stmt.execute_query().iterator(_.string(column)).toSet)
 
-    def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info)
+    def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info): Unit =
     {
       val table = Data.meta_info_table
       db.using_statement(db.insert_permissive(table))(stmt =>
@@ -968,7 +969,7 @@
       })
     }
 
-    def update_sessions(db: SQL.Database, log_name: String, build_info: Build_Info)
+    def update_sessions(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
     {
       val table = Data.sessions_table
       db.using_statement(db.insert_permissive(table))(stmt =>
@@ -999,7 +1000,7 @@
       })
     }
 
-    def update_theories(db: SQL.Database, log_name: String, build_info: Build_Info)
+    def update_theories(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
     {
       val table = Data.theories_table
       db.using_statement(db.insert_permissive(table))(stmt =>
@@ -1023,7 +1024,7 @@
       })
     }
 
-    def update_ml_statistics(db: SQL.Database, log_name: String, build_info: Build_Info)
+    def update_ml_statistics(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
     {
       val table = Data.ml_statistics_table
       db.using_statement(db.insert_permissive(table))(stmt =>
@@ -1042,7 +1043,7 @@
       })
     }
 
-    def write_info(db: SQL.Database, files: List[JFile], ml_statistics: Boolean = false)
+    def write_info(db: SQL.Database, files: List[JFile], ml_statistics: Boolean = false): Unit =
     {
       abstract class Table_Status(table: SQL.Table)
       {
@@ -1052,7 +1053,7 @@
         def required(file: JFile): Boolean = !known(Log_File.plain_name(file.getName))
 
         def update_db(db: SQL.Database, log_file: Log_File): Unit
-        def update(log_file: Log_File)
+        def update(log_file: Log_File): Unit =
         {
           if (!known(log_file.name)) {
             update_db(db, log_file)