# HG changeset patch
# User wenzelm
# Date 1475935661 -7200
# Node ID d54aa68e33dc00340016e4e9424e0849099a2b6e
# Parent  623abb8fecdf9abdd8bc16afcac72b7ef8d9d2a0
tuned;

diff -r 623abb8fecdf -r d54aa68e33dc src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Sat Oct 08 16:02:06 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 16:07:41 2016 +0200
@@ -232,18 +232,18 @@
   object Isatest
   {
     val engine = "isatest"
-    val Test_Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
-    val Test_End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""")
+    val Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
+    val End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""")
     val Isabelle_Version = new Regex("""^Isabelle version: (\S+)$""")
     val No_AFP_Version = new Regex("""$.""")
   }
 
-  object AFP
+  object AFP_Test
   {
     val engine = "afp-test"
-    val Test_Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
-    val Test_Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
-    val Test_End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
+    val Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
+    val Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
+    val End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
     val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""")
     val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""")
     val Bad_Init = new Regex("""^cp:.*: Disc quota exceeded$""")
@@ -252,7 +252,7 @@
   private def parse_meta_info(log_file: Log_File): Meta_Info =
   {
     def parse(engine: String, host: String, start: Date,
-      Test_End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Meta_Info =
+      End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Meta_Info =
     {
       val build_engine = if (engine == "") Nil else List(Field.build_engine -> engine)
       val build_host = if (host == "") Nil else List(Field.build_host -> host)
@@ -260,7 +260,7 @@
       val start_date = List(Field.build_start -> start.toString)
       val end_date =
         log_file.lines.last match {
-          case Test_End(log_file.Strict_Date(end_date)) =>
+          case End(log_file.Strict_Date(end_date)) =>
             List(Field.build_end -> end_date.toString)
           case _ => Nil
         }
@@ -276,19 +276,21 @@
     }
 
     log_file.lines match {
-      case Isatest.Test_Start(log_file.Strict_Date(start), host) :: _ =>
-        parse(Isatest.engine, host, start, Isatest.Test_End,
+      case Isatest.Start(log_file.Strict_Date(start), host) :: _ =>
+        parse(Isatest.engine, host, start, Isatest.End,
           Isatest.Isabelle_Version, Isatest.No_AFP_Version)
 
-      case AFP.Test_Start(log_file.Strict_Date(start), host) :: _ =>
-        parse(AFP.engine, host, start, AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
+      case AFP_Test.Start(log_file.Strict_Date(start), host) :: _ =>
+        parse(AFP_Test.engine, host, start, AFP_Test.End,
+          AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
 
-      case AFP.Test_Start_Old(log_file.Strict_Date(start)) :: _ =>
-        parse(AFP.engine, "", start, AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
+      case AFP_Test.Start_Old(log_file.Strict_Date(start)) :: _ =>
+        parse(AFP_Test.engine, "", start, AFP_Test.End,
+          AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
 
       case line :: _ if line.startsWith("\0") => Meta_Info.empty
-      case List(Isatest.Test_End(_)) => Meta_Info.empty
-      case _ :: AFP.Bad_Init() :: _ => Meta_Info.empty
+      case List(Isatest.End(_)) => Meta_Info.empty
+      case _ :: AFP_Test.Bad_Init() :: _ => Meta_Info.empty
       case Nil => Meta_Info.empty
 
       case _ => log_file.err("cannot detect log header format")