# HG changeset patch
# User wenzelm
# Date 1475602723 -7200
# Node ID 6957bd29a950e6e809083505efb518cdecf97d34
# Parent  fd454d9e97c456e1daa5127baa029bb35432f745
check session name;

diff -r fd454d9e97c4 -r 6957bd29a950 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Oct 04 19:26:19 2016 +0200
+++ b/src/Pure/Tools/build.scala	Tue Oct 04 19:38:43 2016 +0200
@@ -359,18 +359,24 @@
     ml_statistics: List[Properties.T],
     task_statistics: List[Properties.T])
 
-  def parse_session_log(lines: List[String], full: Boolean): Session_Log_Info =
+  def parse_session_log(name0: String, lines: List[String], full: Boolean): Session_Log_Info =
   {
     val xml_cache = new XML.Cache()
     def parse_lines(prfx: String): List[Properties.T] =
       Props.parse_lines(prfx, lines).map(xml_cache.props(_))
 
     val session_name =
-      lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) getOrElse ""
+      lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) match {
+        case None => name0
+        case Some(name) if name0 == "" || name0 == name => name
+        case Some(name) =>
+          error("Session log for " + quote(name0) + " is actually from " + quote(name))
+      }
     val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
     val command_timings = parse_lines("\fcommand_timing = ")
     val ml_statistics = if (full) parse_lines("\fML_statistics = ") else Nil
     val task_statistics = if (full) parse_lines("\ftask_statistics = ") else Nil
+
     Session_Log_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
   }
 
@@ -518,7 +524,7 @@
       }
 
       try {
-        val info = parse_session_log(split_lines(text), false)
+        val info = parse_session_log(name, split_lines(text), false)
         val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
         (info.command_timings, session_timing)
       }
diff -r fd454d9e97c4 -r 6957bd29a950 src/Pure/Tools/ci_api.scala
--- a/src/Pure/Tools/ci_api.scala	Tue Oct 04 19:26:19 2016 +0200
+++ b/src/Pure/Tools/ci_api.scala	Tue Oct 04 19:38:43 2016 +0200
@@ -49,7 +49,7 @@
     {
       val text =
         session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse ""
-      Build.parse_session_log(split_lines(text), full)
+      Build.parse_session_log(name, split_lines(text), full)
     }
   }