--- a/src/Pure/Admin/build_status.scala Sun May 07 21:42:23 2017 +0200
+++ b/src/Pure/Admin/build_status.scala Sun May 07 22:10:48 2017 +0200
@@ -157,6 +157,13 @@
entry.ml_timing.elapsed.minutes,
entry.ml_timing.resources.minutes).mkString(" "))))
+ val max_time =
+ ((0.0 /: session.entries){ case (m, entry) =>
+ m.max(entry.timing.elapsed.minutes).
+ max(entry.timing.resources.minutes).
+ max(entry.ml_timing.elapsed.minutes).
+ max(entry.ml_timing.resources.minutes) } max 0.1) * 1.1
+
def gnuplot(plots: List[String], kind: String): Process_Result =
{
val name = session.name + "_" + kind
@@ -167,8 +174,9 @@
set timefmt "%s"
set format x "%d-%b"
set xlabel """ + quote(session.name) + """ noenhanced
-set key left top
-plot [] [0:] """ + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
+set key left bottom
+plot [] [0:""" + max_time + "] " +
+ plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
val result =
Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))