# HG changeset patch
# User wenzelm
# Date 1495021639 -7200
# Node ID c103358a55594b0ad92a4b89c5a8ee29bbb3e941
# Parent  5414c14c398472477a2bc7f5c09604f5870e7005
tuned signature;

diff -r 5414c14c3984 -r c103358a5559 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Wed May 17 11:53:16 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed May 17 13:47:19 2017 +0200
@@ -488,7 +488,7 @@
     def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
     def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
     def ml_statistics(name: String): ML_Statistics =
-      get_default(name, entry => ML_Statistics(name, entry.ml_statistics), ML_Statistics.empty)
+      get_default(name, entry => ML_Statistics(entry.ml_statistics, name), ML_Statistics.empty)
   }
 
   private def parse_build_info(log_file: Log_File, parse_ml_statistics: Boolean): Build_Info =
diff -r 5414c14c3984 -r c103358a5559 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Wed May 17 11:53:16 2017 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Wed May 17 13:47:19 2017 +0200
@@ -22,10 +22,10 @@
 
   final case class Entry(time: Double, data: Map[String, Double])
 
-  def apply(session_name: String, ml_statistics: List[Properties.T]): ML_Statistics =
-    new ML_Statistics(session_name, ml_statistics)
+  def apply(ml_statistics: List[Properties.T], heading: String = ""): ML_Statistics =
+    new ML_Statistics(ml_statistics, heading)
 
-  val empty = apply("", Nil)
+  val empty = apply(Nil)
 
 
   /* standard fields */
@@ -65,7 +65,7 @@
     List(tasks_fields, workers_fields, heap_fields)
 }
 
-final class ML_Statistics private(val session_name: String, val ml_statistics: List[Properties.T])
+final class ML_Statistics private(val ml_statistics: List[Properties.T], val heading: String)
 {
   val Now = new Properties.Double("now")
   def now(props: Properties.T): Double = Now.unapply(props).get
@@ -142,7 +142,7 @@
       GUI_Thread.later {
         new Frame {
           iconImage = GUI.isabelle_image()
-          title = session_name
+          title = heading
           contents = Component.wrap(new ChartPanel(c))
           visible = true
         }
diff -r 5414c14c3984 -r c103358a5559 src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala	Wed May 17 11:53:16 2017 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Wed May 17 13:47:19 2017 +0200
@@ -54,7 +54,7 @@
   private def update_chart: Unit =
     ML_Statistics.all_fields.find(_._1 == data_name) match {
       case None =>
-      case Some((_, fields)) => ML_Statistics("", statistics.toList).update_data(data, fields)
+      case Some((_, fields)) => ML_Statistics(statistics.toList).update_data(data, fields)
     }
 
   private val input_delay =