more informative timeout message, notably for build_status;
authorwenzelm
Mon Oct 30 19:19:24 2017 +0100 (19 months ago)
changeset 6694405df740cb54b
parent 66943 351aaaa9bacd
child 66945 b6f787a17fbe
more informative timeout message, notably for build_status;
src/Pure/Admin/build_log.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Admin/build_log.scala	Mon Oct 30 18:39:30 2017 +0100
     1.2 +++ b/src/Pure/Admin/build_log.scala	Mon Oct 30 19:19:24 2017 +0100
     1.3 @@ -649,6 +649,10 @@
     1.4      ml_statistics: List[Properties.T],
     1.5      task_statistics: List[Properties.T],
     1.6      errors: List[String])
     1.7 +  {
     1.8 +    def error(s: String): Session_Info =
     1.9 +      copy(errors = errors ::: List(s))
    1.10 +  }
    1.11  
    1.12    private def parse_session_info(
    1.13      log_file: Log_File,
     2.1 --- a/src/Pure/Tools/build.scala	Mon Oct 30 18:39:30 2017 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Mon Oct 30 19:19:24 2017 +0100
     2.3 @@ -536,15 +536,18 @@
     2.4                val database = store.output_dir + store.database(name)
     2.5                database.file.delete
     2.6  
     2.7 +              val build_log =
     2.8 +                Build_Log.Log_File(name, process_result.out_lines).
     2.9 +                  parse_session_info(
    2.10 +                    command_timings = true,
    2.11 +                    theory_timings = true,
    2.12 +                    ml_statistics = true,
    2.13 +                    task_statistics = true)
    2.14 +
    2.15                using(SQLite.open_database(database))(db =>
    2.16                  store.write_session_info(db, name,
    2.17                    build_log =
    2.18 -                    Build_Log.Log_File(name, process_result.out_lines).
    2.19 -                      parse_session_info(
    2.20 -                        command_timings = true,
    2.21 -                        theory_timings = true,
    2.22 -                        ml_statistics = true,
    2.23 -                        task_statistics = true),
    2.24 +                    if (process_result.timeout) build_log.error("Timeout") else build_log,
    2.25                    build =
    2.26                      Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
    2.27                        process_result.rc)))