more specific workaround (see also ed7b5cd3a7f2);
authorwenzelm
Mon May 08 10:23:12 2017 +0200 (2017-05-08)
changeset 657662edb89630a80
parent 65765 c67bb109cd7b
child 65767 222ed8901008
more specific workaround (see also ed7b5cd3a7f2);
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Sun May 07 23:57:20 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Mon May 08 10:23:12 2017 +0200
     1.3 @@ -93,25 +93,23 @@
     1.4          {
     1.5            val res = stmt.execute_query()
     1.6            while (res.next()) {
     1.7 -            val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
     1.8 -
     1.9 +            val session_name = res.string(Build_Log.Data.session_name)
    1.10              val threads =
    1.11              {
    1.12                val threads1 =
    1.13                  res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match {
    1.14 -                  case Threads_Option(Value.Int(i)) => i
    1.15 +                  case Threads_Option(Value.Int(i)) if session_name == "Pure" => i
    1.16                    case _ => 1
    1.17                  }
    1.18                val threads2 = res.get_int(Build_Log.Data.threads).getOrElse(1)
    1.19                threads1 max threads2
    1.20              }
    1.21 -
    1.22 +            val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
    1.23              val data_name =
    1.24                profile.description +
    1.25                  (if (ml_platform.startsWith("x86_64")) ", 64bit" else "") +
    1.26                  (if (threads == 1) "" else ", " + threads + " threads")
    1.27  
    1.28 -            val name = res.string(Build_Log.Data.session_name)
    1.29              val entry =
    1.30                Entry(res.date(Build_Log.Data.pull_date),
    1.31                  res.timing(
    1.32 @@ -124,9 +122,9 @@
    1.33                    Build_Log.Data.ml_timing_gc))
    1.34  
    1.35              val sessions = data_entries.getOrElse(data_name, Map.empty)
    1.36 -            val entries = sessions.get(name).map(_.entries) getOrElse Nil
    1.37 -            val session = Session(name, threads, entry :: entries)
    1.38 -            data_entries += (data_name -> (sessions + (name -> session)))
    1.39 +            val entries = sessions.get(session_name).map(_.entries) getOrElse Nil
    1.40 +            val session = Session(session_name, threads, entry :: entries)
    1.41 +            data_entries += (data_name -> (sessions + (session_name -> session)))
    1.42            }
    1.43          })
    1.44        }