# HG changeset patch
# User wenzelm
# Date 1494171641 -7200
# Node ID a51290fd62d9b568d2c9c738b5a5b870d56925e1
# Parent  a2b041a3652398ec6163cb333ea046bfea604fcf
more uniform charts;
tuned headings;

diff -r a2b041a36523 -r a51290fd62d9 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sun May 07 17:29:38 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Sun May 07 17:40:41 2017 +0200
@@ -161,10 +161,9 @@
                   entries.map(entry =>
                     List(entry.date.unix_epoch.toString,
                       entry.timing.elapsed.minutes,
-                      entry.timing.cpu.minutes,
+                      entry.timing.resources.minutes,
                       entry.ml_timing.elapsed.minutes,
-                      entry.ml_timing.cpu.minutes,
-                      entry.ml_timing.gc.minutes).mkString(" "))))
+                      entry.ml_timing.resources.minutes).mkString(" "))))
 
               def gnuplot(plots: List[String], kind: String): Process_Result =
               {
@@ -196,9 +195,7 @@
                   """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
                   """ using 1:5 smooth csplines title "ML cpu time" """,
                   """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
-                  """ using 1:4 smooth csplines title "ML elapsed time" """,
-                  """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
-                  """ using 1:6 smooth csplines title "ML gc time" """)
+                  """ using 1:4 smooth csplines title "ML elapsed time" """)
 
               List(gnuplot(timing_plots, "timing"), gnuplot(ml_timing_plots, "ml_timing"))
             }
@@ -206,12 +203,11 @@
         }, session_entries).flatten.foreach(_.check)
 
       val sessions = session_entries.toList.sortBy(_._2.head.timing.elapsed.ms).reverse
-      val heading = "Build status for " + data_name + " (" + data.date + ")"
 
       File.write(dir + Path.basic("index.html"),
         HTML.output_document(
-          List(HTML.title(heading)),
-          HTML.chapter(heading) ::
+          List(HTML.title("Isabelle build status for " + data_name)),
+          HTML.chapter("Isabelle build status for " + data_name + " (" + data.date + ")") ::
           HTML.itemize(
             sessions.map({ case (name, entries) =>
               HTML.link("#session_" + name, HTML.text(name)) ::
@@ -230,12 +226,10 @@
                   HTML.image(name + "_ml_timing.png")))) })))
     }
 
-    val heading = "Build status (" + data.date + ")"
-
     File.write(target_dir + Path.basic("index.html"),
       HTML.output_document(
-        List(HTML.title(heading)),
-        List(HTML.chapter(heading),
+        List(HTML.title("Isabelle build status")),
+        List(HTML.chapter("Isabelle build status (" + data.date + ")"),
           HTML.itemize(data_entries.map({ case (name, _) =>
             List(HTML.link(name + "/index.html", HTML.text(name))) })))))
   }