diff -r 84f283385091 -r fd454d9e97c4 src/Pure/Tools/task_statistics.scala
--- a/src/Pure/Tools/task_statistics.scala	Tue Oct 04 18:26:26 2016 +0200
+++ b/src/Pure/Tools/task_statistics.scala	Tue Oct 04 19:26:19 2016 +0200
@@ -17,22 +17,23 @@
 
 object Task_Statistics
 {
-  def apply(name: String, tasks: List[Properties.T]): Task_Statistics =
-    new Task_Statistics(name, tasks)
+  def apply(session_name: String, task_statistics: List[Properties.T]): Task_Statistics =
+    new Task_Statistics(session_name, task_statistics)
 
-  def apply(info: Build.Log_Info): Task_Statistics =
-    apply(info.name, info.tasks)
+  def apply(info: Build.Session_Log_Info): Task_Statistics =
+    apply(info.session_name, info.task_statistics)
 }
 
-final class Task_Statistics private(val name: String, val tasks: List[Properties.T])
+final class Task_Statistics private(
+  val session_name: String, val task_statistics: List[Properties.T])
 {
   private val Task_Name = new Properties.String("task_name")
   private val Run = new Properties.Int("run")
 
   def chart(bins: Int = 100): JFreeChart =
   {
-    val values = new Array[Double](tasks.length)
-    for ((Run(x), i) <- tasks.iterator.zipWithIndex)
+    val values = new Array[Double](task_statistics.length)
+    for ((Run(x), i) <- task_statistics.iterator.zipWithIndex)
       values(i) = java.lang.Math.log10((x max 1).toDouble / 1000000)
 
     val data = new HistogramDataset
@@ -54,7 +55,7 @@
     GUI_Thread.later {
       new Frame {
         iconImage = GUI.isabelle_image()
-        title = name
+        title = session_name
         contents = Component.wrap(new ChartPanel(chart(bins)))
         visible = true
       }