src/Pure/Admin/build_log.scala

           if (ssh_host == "") None
           else Some(SSH.open_session(options, host = ssh_host, user = ssh_user, port = ssh_port)),
         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 =>
           File.find_files(dir.file, pred = Log_File.is_log(_), follow_links = true))
       write_info(db, log_files, ml_statistics = ml_statistics)

       db.create_view(Data.pull_date_table(afp = true))
       db.create_view(Data.universal_table)
     }
 
     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
 
       using(SQLite.open_database(sqlite_database))(db2 =>

 
     def domain(db: SQL.Database, table: SQL.Table, column: SQL.Column): Set[String] =
       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 =>
       {
         stmt.string(1) = log_name

         }
         stmt.execute()
       })
     }
 
-    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 =>
       {
         val sessions =

           stmt.execute()
         }
       })
     }
 
-    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 =>
       {
         val sessions =

           stmt.execute()
         }
       })
     }
 
-    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 =>
       {
         val ml_stats: List[(String, Option[Bytes])] =

           stmt.execute()
         }
       })
     }
 
-    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)
       {
         db.create_table(table)
         private var known: Set[String] = domain(db, table, Data.log_name)
 
         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)
             known += log_file.name
           }