src/Pure/Admin/build_status.scala
changeset 65750 7f5556f4b584
parent 65747 5a3052b2095f
child 65751 426d4bf3b9bb
     1.1 --- a/src/Pure/Admin/build_status.scala	Sat May 06 20:58:34 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sat May 06 21:28:41 2017 +0200
     1.3 @@ -54,7 +54,8 @@
     1.4      progress: Progress = No_Progress,
     1.5      history_length: Int = default_history_length,
     1.6      only_sessions: Set[String] = Set.empty,
     1.7 -    elapsed_threshold: Time = Time.zero): Data =
     1.8 +    elapsed_threshold: Time = Time.zero,
     1.9 +    verbose: Boolean = false): Data =
    1.10    {
    1.11      var data: Data = Map.empty
    1.12  
    1.13 @@ -76,7 +77,10 @@
    1.14              Build_Log.Data.ml_timing_cpu,
    1.15              Build_Log.Data.ml_timing_gc)
    1.16  
    1.17 -        db.using_statement(profile.select(columns, history_length, only_sessions))(stmt =>
    1.18 +        val sql = profile.select(columns, history_length, only_sessions)
    1.19 +        if (verbose) progress.echo(sql)
    1.20 +
    1.21 +        db.using_statement(sql)(stmt =>
    1.22          {
    1.23            val res = stmt.execute_query()
    1.24            while (res.next()) {
    1.25 @@ -230,6 +234,7 @@
    1.26        var history_length = default_history_length
    1.27        var options = Options.init()
    1.28        var image_size = default_image_size
    1.29 +      var verbose = false
    1.30  
    1.31        val getopts = Getopts("""
    1.32  Usage: isabelle build_status [OPTIONS]
    1.33 @@ -243,6 +248,7 @@
    1.34      -m           include ML timing
    1.35      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    1.36      -s WxH       size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """)
    1.37 +    -v           verbose
    1.38  
    1.39    Present performance statistics from build log database, which is specified
    1.40    via system options build_log_database_host, build_log_database_user etc.
    1.41 @@ -258,7 +264,8 @@
    1.42            space_explode('x', arg).map(Value.Int.parse(_)) match {
    1.43              case List(w, h) if w > 0 && h > 0 => image_size = (w, h)
    1.44              case _ => error("Error bad PNG image size: " + quote(arg))
    1.45 -          }))
    1.46 +          }),
    1.47 +        "v" -> (_ => verbose = true))
    1.48  
    1.49        val more_args = getopts(args)
    1.50        if (more_args.nonEmpty) getopts.usage()
    1.51 @@ -267,7 +274,7 @@
    1.52  
    1.53        val data =
    1.54          read_data(options, progress = progress, history_length = history_length,
    1.55 -          only_sessions = only_sessions, elapsed_threshold = elapsed_threshold)
    1.56 +          only_sessions = only_sessions, elapsed_threshold = elapsed_threshold, verbose = verbose)
    1.57  
    1.58        present_data(data, progress = progress, target_dir = target_dir,
    1.59          image_size = image_size, ml_timing = ml_timing)