present ML timing as well;

--- a/src/Pure/Tools/build_stats.scala	Tue Aug 16 12:41:43 2016 +0200
+++ b/src/Pure/Tools/build_stats.scala	Tue Aug 16 15:51:44 2016 +0200
@@ -79,12 +79,14 @@
   private val default_size = (800, 600)
   private val default_only_sessions = Set.empty[String]
   private val default_elapsed_threshold = Time.zero
+  private val default_ml_timing: Option[Boolean] = None
 
   def present_job(job: String, dir: Path,
     history_length: Int = default_history_length,
     size: (Int, Int) = default_size,
     only_sessions: Set[String] = default_only_sessions,
-    elapsed_threshold: Time = default_elapsed_threshold): List[String] =
+    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))
@@ -116,11 +118,34 @@
             for { (t, stats) <- all_build_stats if stats.finished.isDefinedAt(session) }
             yield {
               val finished = stats.finished(session)
-              t.toString + " " + finished.cpu.minutes + " " + finished.elapsed.minutes
+              val timing = stats.timing(session)
+              List(t.toString, finished.elapsed.minutes, finished.cpu.minutes,
+                timing.elapsed.minutes, timing.cpu.minutes, timing.gc.minutes).mkString(" ")
             }
           File.write(data_file, cat_lines(data))
 
-          val data_file_name = quote(File.standard_path(data_file.getAbsolutePath))
+          val plots1 =
+            List(
+              """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
+              """ using 1:2 smooth csplines title "elapsed time" """,
+              """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
+              """ using 1:3 smooth csplines title "cpu time" """)
+          val plots2 =
+            List(
+              """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
+              """ using 1:4 smooth csplines title "ML elapsed time" """,
+              """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
+              """ using 1:5 smooth csplines title "ML cpu time" """,
+              """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
+              """ using 1:6 smooth csplines title "ML gc time" """)
+          val plots =
+            ml_timing match {
+              case None => plots1
+              case Some(false) => plots1 ::: plots2
+              case Some(true) => plots2
+            }
+
+          val data_file_name = File.standard_path(data_file.getAbsolutePath)
           File.write(plot_file, """
 set terminal png size """ + size._1 + "," + size._2 + """
 set output """ + quote(File.standard_path(dir + Path.basic(session + ".png"))) + """
@@ -129,12 +154,7 @@
 set format x "%d-%b"
 set xlabel """ + quote(session) + """ noenhanced
 set key left top
-plot [] [0:] """ +
-  data_file_name + """ using 1:2 smooth sbezier title "interpolated cpu time",""" +
-  data_file_name + """ using 1:2 smooth csplines title "cpu time", """ +
-  data_file_name + """ using 1:3 smooth sbezier title "interpolated elapsed time",""" +
-  data_file_name + """ using 1:3 smooth csplines title "elapsed time"
-""")
+plot [] [0:] """ + plots.map(s => quote(data_file_name) + " " + s).mkString(", ") + "\n")
           val result = Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(plot_file))
           if (result.rc != 0) {
             Output.error_message("Session " + session + ": gnuplot error")
@@ -164,6 +184,7 @@
     Isabelle_Tool("build_stats", "present statistics from session build output", args =>
     {
       var target_dir = Path.explode("stats")
+      var ml_timing = default_ml_timing
       var only_sessions = default_only_sessions
       var elapsed_threshold = default_elapsed_threshold
       var history_length = default_history_length
@@ -174,18 +195,22 @@
 
   Options are:
     -D DIR       target directory (default "stats")
+    -M           only ML timing
     -S SESSIONS  only given SESSIONS (comma separated)
     -T THRESHOLD only sessions with elapsed time >= THRESHOLD (minutes)
     -l LENGTH    length of history (default 100)
+    -m           include ML timing
     -s WxH       size of PNG image (default 800x600)
 
   Present statistics from session build output of the given JOBS, from Jenkins
   continuous build service specified as URL via ISABELLE_JENKINS_ROOT.
 """,
         "D:" -> (arg => target_dir = Path.explode(arg)),
+        "M" -> (_ => ml_timing = Some(true)),
         "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
         "T:" -> (arg => elapsed_threshold = Time.minutes(Properties.Value.Double.parse(arg))),
         "l:" -> (arg => history_length = Properties.Value.Int.parse(arg)),
+        "m" -> (_ => ml_timing = Some(false)),
         "s:" -> (arg =>
           space_explode('x', arg).map(Properties.Value.Int.parse(_)) match {
             case List(w, h) if w > 0 && h > 0 => size = (w, h)
@@ -206,7 +231,8 @@
       for (job <- jobs) {
         val dir = target_dir + Path.basic(job)
         Output.writeln(dir.implode)
-        val sessions = present_job(job, dir, history_length, size, only_sessions, elapsed_threshold)
+        val sessions =
+          present_job(job, dir, history_length, size, only_sessions, elapsed_threshold, ml_timing)
         File.write(dir + Path.basic("index.html"),
           html_header + "\n<h1>" + HTML.output(job) + "</h1>\n" +
           cat_lines(