more uniform threads value, notably for Pure session;
authorwenzelm
Sun May 07 13:42:20 2017 +0200 (2017-05-07)
changeset 65752ed7b5cd3a7f2
parent 65751 426d4bf3b9bb
child 65753 787e5ee6ef53
more uniform threads value, notably for Pure session;
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Sun May 07 13:20:24 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 07 13:42:20 2017 +0200
     1.3 @@ -67,6 +67,7 @@
     1.4          val columns =
     1.5            List(
     1.6              Build_Log.Data.pull_date,
     1.7 +            Build_Log.Settings.ISABELLE_BUILD_OPTIONS,
     1.8              Build_Log.Settings.ML_PLATFORM,
     1.9              Build_Log.Data.session_name,
    1.10              Build_Log.Data.threads,
    1.11 @@ -77,6 +78,8 @@
    1.12              Build_Log.Data.ml_timing_cpu,
    1.13              Build_Log.Data.ml_timing_gc)
    1.14  
    1.15 +        val Threads_Option = """threads\s*=\s*(\d+)""".r
    1.16 +
    1.17          val sql = profile.select(columns, history_length, only_sessions)
    1.18          if (verbose) progress.echo(sql)
    1.19  
    1.20 @@ -85,11 +88,18 @@
    1.21            val res = stmt.execute_query()
    1.22            while (res.next()) {
    1.23              val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
    1.24 -            val threads = res.get_int(Build_Log.Data.threads)
    1.25 +
    1.26 +            val threads_option =
    1.27 +              res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match {
    1.28 +                case Threads_Option(Value.Int(i)) => i
    1.29 +                case _ => 1
    1.30 +              }
    1.31 +            val threads = res.get_int(Build_Log.Data.threads).getOrElse(1)
    1.32 +
    1.33              val name =
    1.34                profile.name +
    1.35                  "_m" + (if (ml_platform.startsWith("x86_64")) "64" else "32") +
    1.36 -                "_M" + threads.getOrElse(1)
    1.37 +                "_M" + (threads_option max threads)
    1.38  
    1.39              val session = res.string(Build_Log.Data.session_name)
    1.40              val entry =