# HG changeset patch
# User wenzelm
# Date 1494157340 -7200
# Node ID ed7b5cd3a7f220fb9833436cd125829ad8530fea
# Parent  426d4bf3b9bb9198f8ccbd39de52f1a36668a2d4
more uniform threads value, notably for Pure session;

diff -r 426d4bf3b9bb -r ed7b5cd3a7f2 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sun May 07 13:20:24 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Sun May 07 13:42:20 2017 +0200
@@ -67,6 +67,7 @@
         val columns =
           List(
             Build_Log.Data.pull_date,
+            Build_Log.Settings.ISABELLE_BUILD_OPTIONS,
             Build_Log.Settings.ML_PLATFORM,
             Build_Log.Data.session_name,
             Build_Log.Data.threads,
@@ -77,6 +78,8 @@
             Build_Log.Data.ml_timing_cpu,
             Build_Log.Data.ml_timing_gc)
 
+        val Threads_Option = """threads\s*=\s*(\d+)""".r
+
         val sql = profile.select(columns, history_length, only_sessions)
         if (verbose) progress.echo(sql)
 
@@ -85,11 +88,18 @@
           val res = stmt.execute_query()
           while (res.next()) {
             val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
-            val threads = res.get_int(Build_Log.Data.threads)
+
+            val threads_option =
+              res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match {
+                case Threads_Option(Value.Int(i)) => i
+                case _ => 1
+              }
+            val threads = res.get_int(Build_Log.Data.threads).getOrElse(1)
+
             val name =
               profile.name +
                 "_m" + (if (ml_platform.startsWith("x86_64")) "64" else "32") +
-                "_M" + threads.getOrElse(1)
+                "_M" + (threads_option max threads)
 
             val session = res.string(Build_Log.Data.session_name)
             val entry =