src/Pure/Tools/build.scala
changeset 65318 342efc382558
parent 65317 b9f5cd845616
child 65320 52861eebf58d
equal deleted inserted replaced
65317:b9f5cd845616 65318:342efc382558
    47             no_timings
    47             no_timings
    48           }
    48           }
    49           try {
    49           try {
    50             using(SQLite.open_database(database))(db =>
    50             using(SQLite.open_database(database))(db =>
    51             {
    51             {
    52               val build_log = store.read_build_log(db, name, command_timings = true)
    52               val build_log = store.read_build_log(db, command_timings = true)
    53               val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0
    53               val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0
    54               (build_log.command_timings, session_timing)
    54               (build_log.command_timings, session_timing)
    55             })
    55             })
    56           }
    56           }
    57           catch {
    57           catch {
   498             {
   498             {
   499               val database = store.output_dir + store.database(name)
   499               val database = store.output_dir + store.database(name)
   500               database.file.delete
   500               database.file.delete
   501 
   501 
   502               using(SQLite.open_database(database))(db =>
   502               using(SQLite.open_database(database))(db =>
   503                 store.write_session_info(db,
   503                 store.write_session_info(db, name,
   504                   build_log =
   504                   build_log =
   505                     Build_Log.Log_File(name, process_result.out_lines).
   505                     Build_Log.Log_File(name, process_result.out_lines).
   506                       parse_session_info(name,
   506                       parse_session_info(
   507                         command_timings = true, ml_statistics = true, task_statistics = true),
   507                         command_timings = true, ml_statistics = true, task_statistics = true),
   508                   build =
   508                   build =
   509                     Session_Info(sources_stamp(name), input_heaps, heap_stamp, process_result.rc)))
   509                     Session_Info(sources_stamp(name), input_heaps, heap_stamp, process_result.rc)))
   510             }
   510             }
   511 
   511