src/Pure/Tools/build.scala
changeset 66944 05df740cb54b
parent 66943 351aaaa9bacd
child 66961 f855f9aed72f
equal deleted inserted replaced
66943:351aaaa9bacd 66944:05df740cb54b
   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