tuned output;
authorwenzelm
Sun May 07 22:10:48 2017 +0200 (2017-05-07)
changeset 65763dbadcc3fbe33
parent 65762 295b845243d3
child 65764 1af6d544c2a3
tuned output;
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Sun May 07 21:42:23 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 07 22:10:48 2017 +0200
     1.3 @@ -157,6 +157,13 @@
     1.4                      entry.ml_timing.elapsed.minutes,
     1.5                      entry.ml_timing.resources.minutes).mkString(" "))))
     1.6  
     1.7 +            val max_time =
     1.8 +              ((0.0 /: session.entries){ case (m, entry) =>
     1.9 +                m.max(entry.timing.elapsed.minutes).
    1.10 +                  max(entry.timing.resources.minutes).
    1.11 +                  max(entry.ml_timing.elapsed.minutes).
    1.12 +                  max(entry.ml_timing.resources.minutes) } max 0.1) * 1.1
    1.13 +
    1.14              def gnuplot(plots: List[String], kind: String): Process_Result =
    1.15              {
    1.16                val name = session.name + "_" + kind
    1.17 @@ -167,8 +174,9 @@
    1.18  set timefmt "%s"
    1.19  set format x "%d-%b"
    1.20  set xlabel """ + quote(session.name) + """ noenhanced
    1.21 -set key left top
    1.22 -plot [] [0:] """ + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
    1.23 +set key left bottom
    1.24 +plot [] [0:""" + max_time + "] " +
    1.25 +                plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
    1.26  
    1.27                val result =
    1.28                  Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))