removed threshold: redundant due to sorting;
authorwenzelm
Sun May 07 17:10:03 2017 +0200 (2017-05-07)
changeset 65758d79126bb5d07
parent 65757 a6522bb9acfa
child 65759 a2b041a36523
removed threshold: redundant due to sorting;
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Sun May 07 17:06:05 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 07 17:10:03 2017 +0200
     1.3 @@ -39,10 +39,6 @@
     1.4      Jenkins.build_status_profiles ::: Isabelle_Cronjob.build_status_profiles
     1.5  
     1.6    sealed case class Entry(date: Date, timing: Timing, ml_timing: Timing)
     1.7 -  {
     1.8 -    def check(elapsed_threshold: Time): Boolean =
     1.9 -      !timing.is_zero && timing.elapsed >= elapsed_threshold
    1.10 -  }
    1.11  
    1.12    sealed case class Data(date: Date, entries: Map[String, Map[String, List[Entry]]])
    1.13    {
    1.14 @@ -59,7 +55,6 @@
    1.15      progress: Progress = No_Progress,
    1.16      history_length: Int = default_history_length,
    1.17      only_sessions: Set[String] = Set.empty,
    1.18 -    elapsed_threshold: Time = Time.zero,
    1.19      verbose: Boolean = false): Data =
    1.20    {
    1.21      val date = Date.now()
    1.22 @@ -133,10 +128,8 @@
    1.23          session_entries1 <-
    1.24            {
    1.25              val session_entries1 =
    1.26 -              for {
    1.27 -                (session, entries) <- session_entries
    1.28 -                if entries.filter(_.check(elapsed_threshold)).length >= 3
    1.29 -              } yield (session, entries)
    1.30 +              for { (session, entries) <- session_entries if entries.length >= 3 }
    1.31 +              yield (session, entries)
    1.32              if (session_entries1.isEmpty) None
    1.33              else Some(session_entries1)
    1.34            }
    1.35 @@ -256,7 +249,6 @@
    1.36        var target_dir = default_target_dir
    1.37        var ml_timing: Option[Boolean] = None
    1.38        var only_sessions = Set.empty[String]
    1.39 -      var elapsed_threshold = Time.zero
    1.40        var history_length = default_history_length
    1.41        var options = Options.init()
    1.42        var image_size = default_image_size
    1.43 @@ -269,7 +261,6 @@
    1.44      -D DIR       target directory (default """ + default_target_dir + """)
    1.45      -M           only ML timing
    1.46      -S SESSIONS  only given SESSIONS (comma separated)
    1.47 -    -T THRESHOLD only sessions with elapsed time >= THRESHOLD (minutes)
    1.48      -l LENGTH    length of history (default """ + default_history_length + """)
    1.49      -m           include ML timing
    1.50      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    1.51 @@ -282,7 +273,6 @@
    1.52          "D:" -> (arg => target_dir = Path.explode(arg)),
    1.53          "M" -> (_ => ml_timing = Some(true)),
    1.54          "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
    1.55 -        "T:" -> (arg => elapsed_threshold = Time.minutes(Value.Double.parse(arg))),
    1.56          "l:" -> (arg => history_length = Value.Int.parse(arg)),
    1.57          "m" -> (_ => ml_timing = Some(false)),
    1.58          "o:" -> (arg => options = options + arg),
    1.59 @@ -300,7 +290,7 @@
    1.60  
    1.61        val data =
    1.62          read_data(options, progress = progress, history_length = history_length,
    1.63 -          only_sessions = only_sessions, elapsed_threshold = elapsed_threshold, verbose = verbose)
    1.64 +          only_sessions = only_sessions, verbose = verbose)
    1.65  
    1.66        present_data(data, progress = progress, target_dir = target_dir,
    1.67          image_size = image_size, ml_timing = ml_timing)