1071 override def update_db(db: SQL.Database, log_file: Log_File): Unit = |
1071 override def update_db(db: SQL.Database, log_file: Log_File): Unit = |
1072 update_theories(db, log_file.name, log_file.parse_build_info()) |
1072 update_theories(db, log_file.name, log_file.parse_build_info()) |
1073 } |
1073 } |
1074 ) ::: ml_statistics_status |
1074 ) ::: ml_statistics_status |
1075 |
1075 |
1076 val file_groups_iterator = |
1076 for (file <- files.iterator if status.exists(_.required(file))) { |
1077 files.filter(file => status.exists(_.required(file))). |
1077 val log_name = Log_File.plain_name(file) |
1078 grouped(options.int("build_log_transaction_size") max 1) |
1078 progress.echo("Log " + quote(log_name), verbose = true) |
1079 |
1079 Exn.result { Log_File(file) } match { |
1080 for (file_group <- file_groups_iterator) { |
1080 case Exn.Res(log_file) => |
1081 val log_files = |
1081 private_data.transaction_lock(db, label = "build_log_database") { |
1082 Par_List.map[JFile, Exn.Result[Log_File]]( |
1082 try { status.foreach(_.update(log_file)) } |
1083 file => Exn.result { Log_File(file) }, file_group) |
1083 catch { case exn: Throwable => add_error(log_name, exn) } |
1084 private_data.transaction_lock(db, label = "build_log_database") { |
1084 } |
1085 for (case Exn.Res(log_file) <- log_files) { |
1085 case Exn.Exn(exn) => add_error(log_name, exn) |
1086 progress.echo("Log " + quote(log_file.name), verbose = true) |
|
1087 try { status.foreach(_.update(log_file)) } |
|
1088 catch { case exn: Throwable => add_error(log_file.name, exn) } |
|
1089 } |
|
1090 } |
|
1091 for (case (file, Exn.Exn(exn)) <- file_group.zip(log_files)) { |
|
1092 add_error(Log_File.plain_name(file), exn) |
|
1093 } |
1086 } |
1094 } |
1087 } |
1095 |
1088 |
1096 errors1 |
1089 errors1 |
1097 } |
1090 } |