simplified default;
authorwenzelm
Mon May 08 21:58:15 2017 +0200 (2017-05-08)
changeset 657824935bac8a850
parent 65781 6cd11999f3a3
child 65783 d3d5cb2d6866
simplified default;
etc/options
src/Pure/Admin/build_status.scala
     1.1 --- a/etc/options	Mon May 08 21:51:26 2017 +0200
     1.2 +++ b/etc/options	Mon May 08 21:58:15 2017 +0200
     1.3 @@ -244,3 +244,4 @@
     1.4  option build_log_ssh_host : string = ""
     1.5  option build_log_ssh_user : string = ""
     1.6  option build_log_ssh_port : int = 0
     1.7 +option build_log_history : int = 30  -- "length of relevant history (in days)"
     2.1 --- a/src/Pure/Admin/build_status.scala	Mon May 08 21:51:26 2017 +0200
     2.2 +++ b/src/Pure/Admin/build_status.scala	Mon May 08 21:58:15 2017 +0200
     2.3 @@ -10,7 +10,6 @@
     2.4  object Build_Status
     2.5  {
     2.6    private val default_target_dir = Path.explode("build_status")
     2.7 -  private val default_history_length = 30
     2.8    private val default_image_size = (800, 600)
     2.9  
    2.10  
    2.11 @@ -60,7 +59,6 @@
    2.12    def read_data(options: Options,
    2.13      profiles: List[Profile] = standard_profiles,
    2.14      progress: Progress = No_Progress,
    2.15 -    history_length: Int = default_history_length,
    2.16      only_sessions: Set[String] = Set.empty,
    2.17      verbose: Boolean = false): Data =
    2.18    {
    2.19 @@ -89,7 +87,7 @@
    2.20  
    2.21          val Threads_Option = """threads\s*=\s*(\d+)""".r
    2.22  
    2.23 -        val sql = profile.select(columns, history_length, only_sessions)
    2.24 +        val sql = profile.select(columns, options.int("build_log_history"), only_sessions)
    2.25          if (verbose) progress.echo(sql)
    2.26  
    2.27          db.using_statement(sql)(stmt =>
    2.28 @@ -275,7 +273,6 @@
    2.29      {
    2.30        var target_dir = default_target_dir
    2.31        var only_sessions = Set.empty[String]
    2.32 -      var history_length = default_history_length
    2.33        var options = Options.init()
    2.34        var image_size = default_image_size
    2.35        var verbose = false
    2.36 @@ -286,17 +283,16 @@
    2.37    Options are:
    2.38      -D DIR       target directory (default """ + default_target_dir + """)
    2.39      -S SESSIONS  only given SESSIONS (comma separated)
    2.40 -    -l LENGTH    length of history (default """ + default_history_length + """)
    2.41      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    2.42      -s WxH       size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """)
    2.43      -v           verbose
    2.44  
    2.45    Present performance statistics from build log database, which is specified
    2.46 -  via system options build_log_database_host, build_log_database_user etc.
    2.47 +  via system options build_log_database_host, build_log_database_user,
    2.48 +  build_log_history etc.
    2.49  """,
    2.50          "D:" -> (arg => target_dir = Path.explode(arg)),
    2.51          "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
    2.52 -        "l:" -> (arg => history_length = Value.Int.parse(arg)),
    2.53          "o:" -> (arg => options = options + arg),
    2.54          "s:" -> (arg =>
    2.55            space_explode('x', arg).map(Value.Int.parse(_)) match {
    2.56 @@ -311,8 +307,7 @@
    2.57        val progress = new Console_Progress
    2.58  
    2.59        val data =
    2.60 -        read_data(options, progress = progress, history_length = history_length,
    2.61 -          only_sessions = only_sessions, verbose = verbose)
    2.62 +        read_data(options, progress = progress, only_sessions = only_sessions, verbose = verbose)
    2.63  
    2.64        present_data(data, progress = progress, target_dir = target_dir, image_size = image_size)
    2.65