src/Pure/Admin/build_log.scala
changeset 78984 417b490c9b89
parent 78921 2fee5fba3116
child 78985 24e686fe043e
equal deleted inserted replaced
78983:295aa95cbff9 78984:417b490c9b89
  1042           }
  1042           }
  1043         }
  1043         }
  1044       }
  1044       }
  1045 
  1045 
  1046       val ml_statistics_status =
  1046       val ml_statistics_status =
  1047         if (ml_statistics) Nil
  1047         if (ml_statistics) {
  1048         else {
       
  1049           List(
  1048           List(
  1050             new Table_Status(private_data.ml_statistics_table) {
  1049             new Table_Status(private_data.ml_statistics_table) {
  1051               override def update_db(db: SQL.Database, log_file: Log_File): Unit =
  1050               override def update_db(db: SQL.Database, log_file: Log_File): Unit =
  1052                 update_ml_statistics(db, log_file.name,
  1051                 update_ml_statistics(db, log_file.name,
  1053                   log_file.parse_build_info(ml_statistics = true))
  1052                   log_file.parse_build_info(ml_statistics = true))
  1054             })
  1053             })
  1055         }
  1054         }
       
  1055         else Nil
  1056       val status =
  1056       val status =
  1057         List(
  1057         List(
  1058           new Table_Status(private_data.meta_info_table) {
  1058           new Table_Status(private_data.meta_info_table) {
  1059             override def update_db(db: SQL.Database, log_file: Log_File): Unit =
  1059             override def update_db(db: SQL.Database, log_file: Log_File): Unit =
  1060               update_meta_info(db, log_file.name, log_file.parse_meta_info())
  1060               update_meta_info(db, log_file.name, log_file.parse_meta_info())