# HG changeset patch
# User wenzelm
# Date 1494231792 -7200
# Node ID 2edb89630a80c96aef7d80cb9c1f884dceb90abd
# Parent  c67bb109cd7b912fbc1bd9bcbbdf5d1b3c1ba0d1
more specific workaround (see also ed7b5cd3a7f2);

diff -r c67bb109cd7b -r 2edb89630a80 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sun May 07 23:57:20 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Mon May 08 10:23:12 2017 +0200
@@ -93,25 +93,23 @@
         {
           val res = stmt.execute_query()
           while (res.next()) {
-            val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
-
+            val session_name = res.string(Build_Log.Data.session_name)
             val threads =
             {
               val threads1 =
                 res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match {
-                  case Threads_Option(Value.Int(i)) => i
+                  case Threads_Option(Value.Int(i)) if session_name == "Pure" => i
                   case _ => 1
                 }
               val threads2 = res.get_int(Build_Log.Data.threads).getOrElse(1)
               threads1 max threads2
             }
-
+            val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
             val data_name =
               profile.description +
                 (if (ml_platform.startsWith("x86_64")) ", 64bit" else "") +
                 (if (threads == 1) "" else ", " + threads + " threads")
 
-            val name = res.string(Build_Log.Data.session_name)
             val entry =
               Entry(res.date(Build_Log.Data.pull_date),
                 res.timing(
@@ -124,9 +122,9 @@
                   Build_Log.Data.ml_timing_gc))
 
             val sessions = data_entries.getOrElse(data_name, Map.empty)
-            val entries = sessions.get(name).map(_.entries) getOrElse Nil
-            val session = Session(name, threads, entry :: entries)
-            data_entries += (data_name -> (sessions + (name -> session)))
+            val entries = sessions.get(session_name).map(_.entries) getOrElse Nil
+            val session = Session(session_name, threads, entry :: entries)
+            data_entries += (data_name -> (sessions + (session_name -> session)))
           }
         })
       }