src/Pure/Admin/build_status.scala
changeset 65785 6107504371fb
parent 65784 4763e51ceb78
child 65786 84a0ac8a046e
     1.1 --- a/src/Pure/Admin/build_status.scala	Mon May 08 22:31:54 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Tue May 09 11:21:42 2017 +0200
     1.3 @@ -9,8 +9,28 @@
     1.4  
     1.5  object Build_Status
     1.6  {
     1.7 -  private val default_target_dir = Path.explode("build_status")
     1.8 -  private val default_image_size = (800, 600)
     1.9 +  /* build status */
    1.10 +
    1.11 +  val default_target_dir = Path.explode("build_status")
    1.12 +  val default_image_size = (800, 600)
    1.13 +
    1.14 +  def default_profiles: List[Profile] =
    1.15 +    Jenkins.build_status_profiles ::: Isabelle_Cronjob.build_status_profiles
    1.16 +
    1.17 +  def build_status(options: Options,
    1.18 +    progress: Progress = No_Progress,
    1.19 +    profiles: List[Profile] = default_profiles,
    1.20 +    only_sessions: Set[String] = Set.empty,
    1.21 +    verbose: Boolean = false,
    1.22 +    target_dir: Path = default_target_dir,
    1.23 +    image_size: (Int, Int) = default_image_size)
    1.24 +  {
    1.25 +    val data =
    1.26 +      read_data(options, progress = progress, profiles = profiles,
    1.27 +        only_sessions = only_sessions, verbose = verbose)
    1.28 +
    1.29 +    present_data(data, progress = progress, target_dir = target_dir, image_size = image_size)
    1.30 +  }
    1.31  
    1.32  
    1.33    /* data profiles */
    1.34 @@ -37,9 +57,6 @@
    1.35      }
    1.36    }
    1.37  
    1.38 -  val standard_profiles: List[Profile] =
    1.39 -    Jenkins.build_status_profiles ::: Isabelle_Cronjob.build_status_profiles
    1.40 -
    1.41  
    1.42    sealed case class Data(date: Date, entries: List[(String, List[Session])])
    1.43    sealed case class Session(name: String, threads: Int, entries: List[Entry])
    1.44 @@ -57,8 +74,8 @@
    1.45    /* read data */
    1.46  
    1.47    def read_data(options: Options,
    1.48 -    profiles: List[Profile] = standard_profiles,
    1.49      progress: Progress = No_Progress,
    1.50 +    profiles: List[Profile] = default_profiles,
    1.51      only_sessions: Set[String] = Set.empty,
    1.52      verbose: Boolean = false): Data =
    1.53    {
    1.54 @@ -306,10 +323,8 @@
    1.55  
    1.56        val progress = new Console_Progress
    1.57  
    1.58 -      val data =
    1.59 -        read_data(options, progress = progress, only_sessions = only_sessions, verbose = verbose)
    1.60 -
    1.61 -      present_data(data, progress = progress, target_dir = target_dir, image_size = image_size)
    1.62 +      build_status(options, progress = progress, only_sessions = only_sessions, verbose = verbose,
    1.63 +        target_dir = target_dir, image_size = image_size)
    1.64  
    1.65    }, admin = true)
    1.66  }