# HG changeset patch # User wenzelm # Date 1494273495 -7200 # Node ID 4935bac8a85039fbb17cf92bd5275f4a9194eaf2 # Parent 6cd11999f3a37876ef4704f5a42b854d080b80f2 simplified default; diff -r 6cd11999f3a3 -r 4935bac8a850 etc/options --- a/etc/options Mon May 08 21:51:26 2017 +0200 +++ b/etc/options Mon May 08 21:58:15 2017 +0200 @@ -244,3 +244,4 @@ option build_log_ssh_host : string = "" option build_log_ssh_user : string = "" option build_log_ssh_port : int = 0 +option build_log_history : int = 30 -- "length of relevant history (in days)" diff -r 6cd11999f3a3 -r 4935bac8a850 src/Pure/Admin/build_status.scala --- a/src/Pure/Admin/build_status.scala Mon May 08 21:51:26 2017 +0200 +++ b/src/Pure/Admin/build_status.scala Mon May 08 21:58:15 2017 +0200 @@ -10,7 +10,6 @@ object Build_Status { private val default_target_dir = Path.explode("build_status") - private val default_history_length = 30 private val default_image_size = (800, 600) @@ -60,7 +59,6 @@ def read_data(options: Options, profiles: List[Profile] = standard_profiles, progress: Progress = No_Progress, - history_length: Int = default_history_length, only_sessions: Set[String] = Set.empty, verbose: Boolean = false): Data = { @@ -89,7 +87,7 @@ val Threads_Option = """threads\s*=\s*(\d+)""".r - val sql = profile.select(columns, history_length, only_sessions) + val sql = profile.select(columns, options.int("build_log_history"), only_sessions) if (verbose) progress.echo(sql) db.using_statement(sql)(stmt => @@ -275,7 +273,6 @@ { var target_dir = default_target_dir var only_sessions = Set.empty[String] - var history_length = default_history_length var options = Options.init() var image_size = default_image_size var verbose = false @@ -286,17 +283,16 @@ Options are: -D DIR target directory (default """ + default_target_dir + """) -S SESSIONS only given SESSIONS (comma separated) - -l LENGTH length of history (default """ + default_history_length + """) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -s WxH size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """) -v verbose Present performance statistics from build log database, which is specified - via system options build_log_database_host, build_log_database_user etc. + via system options build_log_database_host, build_log_database_user, + build_log_history etc. """, "D:" -> (arg => target_dir = Path.explode(arg)), "S:" -> (arg => only_sessions = space_explode(',', arg).toSet), - "l:" -> (arg => history_length = Value.Int.parse(arg)), "o:" -> (arg => options = options + arg), "s:" -> (arg => space_explode('x', arg).map(Value.Int.parse(_)) match { @@ -311,8 +307,7 @@ val progress = new Console_Progress val data = - read_data(options, progress = progress, history_length = history_length, - only_sessions = only_sessions, verbose = verbose) + read_data(options, progress = progress, only_sessions = only_sessions, verbose = verbose) present_data(data, progress = progress, target_dir = target_dir, image_size = image_size)