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,