534 // write database |
534 // write database |
535 { |
535 { |
536 val database = store.output_dir + store.database(name) |
536 val database = store.output_dir + store.database(name) |
537 database.file.delete |
537 database.file.delete |
538 |
538 |
|
539 val build_log = |
|
540 Build_Log.Log_File(name, process_result.out_lines). |
|
541 parse_session_info( |
|
542 command_timings = true, |
|
543 theory_timings = true, |
|
544 ml_statistics = true, |
|
545 task_statistics = true) |
|
546 |
539 using(SQLite.open_database(database))(db => |
547 using(SQLite.open_database(database))(db => |
540 store.write_session_info(db, name, |
548 store.write_session_info(db, name, |
541 build_log = |
549 build_log = |
542 Build_Log.Log_File(name, process_result.out_lines). |
550 if (process_result.timeout) build_log.error("Timeout") else build_log, |
543 parse_session_info( |
|
544 command_timings = true, |
|
545 theory_timings = true, |
|
546 ml_statistics = true, |
|
547 task_statistics = true), |
|
548 build = |
551 build = |
549 Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp, |
552 Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp, |
550 process_result.rc))) |
553 process_result.rc))) |
551 } |
554 } |
552 |
555 |