equal
deleted
inserted
replaced
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 object Build_Status |
10 object Build_Status |
11 { |
11 { |
12 private val default_target_dir = Path.explode("build_status") |
12 /* build status */ |
13 private val default_image_size = (800, 600) |
13 |
|
14 val default_target_dir = Path.explode("build_status") |
|
15 val default_image_size = (800, 600) |
|
16 |
|
17 def default_profiles: List[Profile] = |
|
18 Jenkins.build_status_profiles ::: Isabelle_Cronjob.build_status_profiles |
|
19 |
|
20 def build_status(options: Options, |
|
21 progress: Progress = No_Progress, |
|
22 profiles: List[Profile] = default_profiles, |
|
23 only_sessions: Set[String] = Set.empty, |
|
24 verbose: Boolean = false, |
|
25 target_dir: Path = default_target_dir, |
|
26 image_size: (Int, Int) = default_image_size) |
|
27 { |
|
28 val data = |
|
29 read_data(options, progress = progress, profiles = profiles, |
|
30 only_sessions = only_sessions, verbose = verbose) |
|
31 |
|
32 present_data(data, progress = progress, target_dir = target_dir, image_size = image_size) |
|
33 } |
14 |
34 |
15 |
35 |
16 /* data profiles */ |
36 /* data profiles */ |
17 |
37 |
18 def clean_name(name: String): String = |
38 def clean_name(name: String): String = |
35 " AND " + sql_sessions + SQL.enclose(sql) + |
55 " AND " + sql_sessions + SQL.enclose(sql) + |
36 " ORDER BY " + Build_Log.Data.pull_date + " DESC") |
56 " ORDER BY " + Build_Log.Data.pull_date + " DESC") |
37 } |
57 } |
38 } |
58 } |
39 |
59 |
40 val standard_profiles: List[Profile] = |
|
41 Jenkins.build_status_profiles ::: Isabelle_Cronjob.build_status_profiles |
|
42 |
|
43 |
60 |
44 sealed case class Data(date: Date, entries: List[(String, List[Session])]) |
61 sealed case class Data(date: Date, entries: List[(String, List[Session])]) |
45 sealed case class Session(name: String, threads: Int, entries: List[Entry]) |
62 sealed case class Session(name: String, threads: Int, entries: List[Entry]) |
46 { |
63 { |
47 def timing: Timing = if (entries.isEmpty) Timing.zero else entries.head.timing |
64 def timing: Timing = if (entries.isEmpty) Timing.zero else entries.head.timing |
55 |
72 |
56 |
73 |
57 /* read data */ |
74 /* read data */ |
58 |
75 |
59 def read_data(options: Options, |
76 def read_data(options: Options, |
60 profiles: List[Profile] = standard_profiles, |
|
61 progress: Progress = No_Progress, |
77 progress: Progress = No_Progress, |
|
78 profiles: List[Profile] = default_profiles, |
62 only_sessions: Set[String] = Set.empty, |
79 only_sessions: Set[String] = Set.empty, |
63 verbose: Boolean = false): Data = |
80 verbose: Boolean = false): Data = |
64 { |
81 { |
65 val date = Date.now() |
82 val date = Date.now() |
66 var data_entries = Map.empty[String, Map[String, Session]] |
83 var data_entries = Map.empty[String, Map[String, Session]] |
304 val more_args = getopts(args) |
321 val more_args = getopts(args) |
305 if (more_args.nonEmpty) getopts.usage() |
322 if (more_args.nonEmpty) getopts.usage() |
306 |
323 |
307 val progress = new Console_Progress |
324 val progress = new Console_Progress |
308 |
325 |
309 val data = |
326 build_status(options, progress = progress, only_sessions = only_sessions, verbose = verbose, |
310 read_data(options, progress = progress, only_sessions = only_sessions, verbose = verbose) |
327 target_dir = target_dir, image_size = image_size) |
311 |
|
312 present_data(data, progress = progress, target_dir = target_dir, image_size = image_size) |
|
313 |
328 |
314 }, admin = true) |
329 }, admin = true) |
315 } |
330 } |