clarified modules;

--- a/src/Pure/Tools/build_log.scala	Wed Oct 05 13:56:19 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Wed Oct 05 14:15:54 2016 +0200
@@ -7,6 +7,10 @@
 package isabelle
 
 
+import scala.collection.mutable
+import scala.util.matching.Regex
+
+
 object Build_Log
 {
   /* inlined properties (YXML) */
@@ -55,4 +59,74 @@
 
     Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
   }
+
+
+  /* main log: produced by isatest, afp-test, jenkins etc. */
+
+  sealed case class Info(
+    ml_options: List[(String, String)],
+    finished: Map[String, Timing],
+    timing: Map[String, Timing],
+    threads: Map[String, Int])
+  {
+    val sessions: Set[String] = finished.keySet ++ timing.keySet
+
+    override def toString: String =
+      sessions.toList.sorted.mkString("Build_Log.Info(", ", ", ")")
+  }
+
+  private val Session_Finished1 =
+    new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
+  private val Session_Finished2 =
+    new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
+  private val Session_Timing =
+    new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
+
+  private object ML_Option
+  {
+    def unapply(s: String): Option[(String, String)] =
+      s.indexOf('=') match {
+        case -1 => None
+        case i =>
+          val a = s.substring(0, i)
+          Library.try_unquote(s.substring(i + 1)) match {
+            case Some(b) if Build.ml_options.contains(a) => Some((a, b))
+            case _ => None
+          }
+      }
+  }
+
+  def parse_info(text: String): Info =
+  {
+    val ml_options = new mutable.ListBuffer[(String, String)]
+    var finished = Map.empty[String, Timing]
+    var timing = Map.empty[String, Timing]
+    var threads = Map.empty[String, Int]
+
+    for (line <- split_lines(text)) {
+      line match {
+        case Session_Finished1(name,
+            Value.Int(e1), Value.Int(e2), Value.Int(e3),
+            Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
+          val elapsed = Time.hms(e1, e2, e3)
+          val cpu = Time.hms(c1, c2, c3)
+          finished += (name -> Timing(elapsed, cpu, Time.zero))
+        case Session_Finished2(name,
+            Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
+          val elapsed = Time.hms(e1, e2, e3)
+          finished += (name -> Timing(elapsed, Time.zero, Time.zero))
+        case Session_Timing(name,
+            Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
+          val elapsed = Time.seconds(e)
+          val cpu = Time.seconds(c)
+          val gc = Time.seconds(g)
+          timing += (name -> Timing(elapsed, cpu, gc))
+          threads += (name -> t)
+        case ML_Option(a, b) => ml_options += (a -> b)
+        case _ =>
+      }
+    }
+
+    Info(ml_options.toList, finished, timing, threads)
+  }
 }

--- a/src/Pure/Tools/build_stats.scala	Wed Oct 05 13:56:19 2016 +0200
+++ b/src/Pure/Tools/build_stats.scala	Wed Oct 05 14:15:54 2016 +0200
@@ -7,70 +7,8 @@
 package isabelle
 
 
-import scala.collection.mutable
-import scala.util.matching.Regex
-
-
 object Build_Stats
 {
-  /* parse build output */
-
-  private val Session_Finished1 =
-    new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
-  private val Session_Finished2 =
-    new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
-  private val Session_Timing =
-    new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
-
-  private object ML_Option
-  {
-    def unapply(s: String): Option[(String, String)] =
-      s.indexOf('=') match {
-        case -1 => None
-        case i =>
-          val a = s.substring(0, i)
-          Library.try_unquote(s.substring(i + 1)) match {
-            case Some(b) if Build.ml_options.contains(a) => Some((a, b))
-            case _ => None
-          }
-      }
-  }
-
-  def parse(text: String): Build_Stats =
-  {
-    val ml_options = new mutable.ListBuffer[(String, String)]
-    var finished = Map.empty[String, Timing]
-    var timing = Map.empty[String, Timing]
-    var threads = Map.empty[String, Int]
-
-    for (line <- split_lines(text)) {
-      line match {
-        case Session_Finished1(name,
-            Value.Int(e1), Value.Int(e2), Value.Int(e3),
-            Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
-          val elapsed = Time.hms(e1, e2, e3)
-          val cpu = Time.hms(c1, c2, c3)
-          finished += (name -> Timing(elapsed, cpu, Time.zero))
-        case Session_Finished2(name,
-            Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
-          val elapsed = Time.hms(e1, e2, e3)
-          finished += (name -> Timing(elapsed, Time.zero, Time.zero))
-        case Session_Timing(name,
-            Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
-          val elapsed = Time.seconds(e)
-          val cpu = Time.seconds(c)
-          val gc = Time.seconds(g)
-          timing += (name -> Timing(elapsed, cpu, gc))
-          threads += (name -> t)
-        case ML_Option(a, b) => ml_options += (a -> b)
-        case _ =>
-      }
-    }
-
-    Build_Stats(ml_options.toList, finished, timing, threads)
-  }
-
-
   /* presentation */
 
   private val default_history_length = 100
@@ -86,18 +24,18 @@
     elapsed_threshold: Time = default_elapsed_threshold,
     ml_timing: Option[Boolean] = default_ml_timing): List[String] =
   {
-    val build_infos = CI_API.build_job_builds(job).sortBy(_.timestamp).reverse.take(history_length)
-    if (build_infos.isEmpty) error("No build infos for job " + quote(job))
+    val job_infos = CI_API.build_job_builds(job).sortBy(_.timestamp).reverse.take(history_length)
+    if (job_infos.isEmpty) error("No build infos for job " + quote(job))
 
-    val all_build_stats =
-      Par_List.map((info: CI_API.Build_Info) =>
-        (info.timestamp / 1000, parse(Url.read(info.output))), build_infos)
+    val all_infos =
+      Par_List.map((job_info: CI_API.Job_Info) =>
+        (job_info.timestamp / 1000, Build_Log.parse_info(Url.read(job_info.output))), job_infos)
     val all_sessions =
-      (Set.empty[String] /: all_build_stats)(
-        { case (s, (_, stats)) => s ++ stats.sessions })
+      (Set.empty[String] /: all_infos)(
+        { case (s, (_, info)) => s ++ info.sessions })
 
-    def check_threshold(stats: Build_Stats, session: String): Boolean =
-      stats.finished.get(session) match {
+    def check_threshold(info: Build_Log.Info, session: String): Boolean =
+      info.finished.get(session) match {
         case Some(t) => t.elapsed >= elapsed_threshold
         case None => false
       }
@@ -105,7 +43,7 @@
     val sessions =
       for {
         session <- (if (only_sessions.isEmpty) all_sessions else all_sessions & only_sessions)
-        if all_build_stats.filter({ case (_, stats) => check_threshold(stats, session) }).length >= 3
+        if all_infos.filter({ case (_, info) => check_threshold(info, session) }).length >= 3
       } yield session
 
     Isabelle_System.mkdirs(dir)
@@ -113,10 +51,10 @@
       Isabelle_System.with_tmp_file(session, "png") { data_file =>
         Isabelle_System.with_tmp_file(session, "gnuplot") { plot_file =>
           val data =
-            for { (t, stats) <- all_build_stats if stats.finished.isDefinedAt(session) }
+            for { (t, info) <- all_infos if info.finished.isDefinedAt(session) }
             yield {
-              val finished = stats.finished.getOrElse(session, Timing.zero)
-              val timing = stats.timing.getOrElse(session, Timing.zero)
+              val finished = info.finished.getOrElse(session, Timing.zero)
+              val timing = info.timing.getOrElse(session, Timing.zero)
               List(t.toString, finished.elapsed.minutes, finished.cpu.minutes,
                 timing.elapsed.minutes, timing.cpu.minutes, timing.gc.minutes).mkString(" ")
             }
@@ -247,15 +185,3 @@
         "\n</ul>\n" + html_footer)
   })
 }
-
-sealed case class Build_Stats(
-  ml_options: List[(String, String)],
-  finished: Map[String, Timing],
-  timing: Map[String, Timing],
-  threads: Map[String, Int])
-{
-  val sessions: Set[String] = finished.keySet ++ timing.keySet
-
-  override def toString: String =
-    sessions.toList.sorted.mkString("Build_Stats(", ", ", ")")
-}

--- a/src/Pure/Tools/ci_api.scala	Wed Oct 05 13:56:19 2016 +0200
+++ b/src/Pure/Tools/ci_api.scala	Wed Oct 05 14:15:54 2016 +0200
@@ -38,7 +38,7 @@
       name <- JSON.string(job, "name")
     } yield name
 
-  sealed case class Build_Info(
+  sealed case class Job_Info(
     job_name: String,
     timestamp: Long,
     output: URL,
@@ -53,7 +53,7 @@
     }
   }
 
-  def build_job_builds(job_name: String): List[Build_Info] =
+  def build_job_builds(job_name: String): List[Job_Info] =
   {
     val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""")
 
@@ -71,7 +71,7 @@
           log_path <- JSON.string(artifact, "relativePath")
           session <- (log_path match { case Log_Session(name) => Some(name) case _ => None })
         } yield (session -> Url(job_prefix + "/artifact/" + log_path))
-      Build_Info(job_name, timestamp, output, session_logs)
+      Job_Info(job_name, timestamp, output, session_logs)
     }
   }
 }