# HG changeset patch
# User wenzelm
# Date 1509387564 -3600
# Node ID 05df740cb54b0585870109ad700f1a01536a9971
# Parent  351aaaa9bacdcee775f1119c5645edb9bf423d3f
more informative timeout message, notably for build_status;

diff -r 351aaaa9bacd -r 05df740cb54b src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon Oct 30 18:39:30 2017 +0100
+++ b/src/Pure/Admin/build_log.scala	Mon Oct 30 19:19:24 2017 +0100
@@ -649,6 +649,10 @@
     ml_statistics: List[Properties.T],
     task_statistics: List[Properties.T],
     errors: List[String])
+  {
+    def error(s: String): Session_Info =
+      copy(errors = errors ::: List(s))
+  }
 
   private def parse_session_info(
     log_file: Log_File,
diff -r 351aaaa9bacd -r 05df740cb54b src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Oct 30 18:39:30 2017 +0100
+++ b/src/Pure/Tools/build.scala	Mon Oct 30 19:19:24 2017 +0100
@@ -536,15 +536,18 @@
               val database = store.output_dir + store.database(name)
               database.file.delete
 
+              val build_log =
+                Build_Log.Log_File(name, process_result.out_lines).
+                  parse_session_info(
+                    command_timings = true,
+                    theory_timings = true,
+                    ml_statistics = true,
+                    task_statistics = true)
+
               using(SQLite.open_database(database))(db =>
                 store.write_session_info(db, name,
                   build_log =
-                    Build_Log.Log_File(name, process_result.out_lines).
-                      parse_session_info(
-                        command_timings = true,
-                        theory_timings = true,
-                        ml_statistics = true,
-                        task_statistics = true),
+                    if (process_result.timeout) build_log.error("Timeout") else build_log,
                   build =
                     Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
                       process_result.rc)))