less restrictive filter: omit empty charts, but show latest timing;
authorwenzelm
Tue May 16 22:57:12 2017 +0200 (2017-05-16)
changeset 65847ad35427dbe88
parent 65846 aa6e58dc54d0
child 65848 861a3ee712dd
less restrictive filter: omit empty charts, but show latest timing;
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Tue May 16 16:28:13 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Tue May 16 22:57:12 2017 +0200
     1.3 @@ -180,8 +180,7 @@
     1.4      val sorted_entries =
     1.5        (for {
     1.6          (name, sessions) <- data_entries.toList
     1.7 -        sorted_sessions <-
     1.8 -          proper_list(sessions.toList.map(_._2).filter(_.check_timing).sortBy(_.order))
     1.9 +        sorted_sessions <- proper_list(sessions.toList.map(_._2).sortBy(_.order))
    1.10        }
    1.11        yield {
    1.12          val hosts = get_hosts(name).toList.sorted
    1.13 @@ -297,9 +296,11 @@
    1.14                    """ using 1:6 smooth csplines title "heap" """)
    1.15  
    1.16                val plot_names =
    1.17 -                List(
    1.18 -                  gnuplot(timing_plots, "timing", timing_range),
    1.19 -                  gnuplot(ml_timing_plots, "ml_timing", timing_range)) :::
    1.20 +                (if (session.check_timing)
    1.21 +                  List(
    1.22 +                    gnuplot(timing_plots, "timing", timing_range),
    1.23 +                    gnuplot(ml_timing_plots, "ml_timing", timing_range))
    1.24 +                 else Nil) :::
    1.25                  (if (session.check_heap) List(gnuplot(heap_plots, "heap", "[0:]")) else Nil)
    1.26  
    1.27                session.name -> plot_names