# HG changeset patch
# User wenzelm
# Date 1358548397 -3600
# Node ID a7aa17a1f721284794128e5c3e157006db908be9
# Parent  1791a90a94fbcc7967aba53a83c198d6b5ab3b60
use inlined session name as title for charts;
tuned signature;

diff -r 1791a90a94fb -r a7aa17a1f721 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Fri Jan 18 22:38:34 2013 +0100
+++ b/src/Pure/Tools/build.ML	Fri Jan 18 23:33:17 2013 +0100
@@ -98,6 +98,7 @@
           [] => ()
         | dups => error ("Duplicate document variants: " ^ commas_quote dups));
 
+      val _ = writeln ("\fSession.name = " ^ name);
       val _ =
         (case Session.path () of
           [] => ()
diff -r 1791a90a94fb -r a7aa17a1f721 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Jan 18 22:38:34 2013 +0100
+++ b/src/Pure/Tools/build.scala	Fri Jan 18 23:33:17 2013 +0100
@@ -558,19 +558,22 @@
   private def log(name: String): Path = LOG + Path.basic(name)
   private def log_gz(name: String): Path = log(name).ext("gz")
 
+  private val SESSION_NAME = "\fSession.name = "
   private val SESSION_PARENT_PATH = "\fSession.parent_path = "
 
 
   sealed case class Log_Info(
-    stats: List[Properties.T], tasks: List[Properties.T], timing: Properties.T)
+    name: String, stats: List[Properties.T], tasks: List[Properties.T], timing: Properties.T)
 
   def parse_log(text: String): Log_Info =
   {
     val lines = split_lines(text)
+    val name =
+      lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) getOrElse ""
     val stats = Props.parse_lines("\fML_statistics = ", lines)
     val tasks = Props.parse_lines("\ftask_statistics = ", lines)
     val timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
-    Log_Info(stats, tasks, timing)
+    Log_Info(name, stats, tasks, timing)
   }
 
 
@@ -694,8 +697,8 @@
 
                 val parent_path =
                   if (job.info.options.bool("browser_info"))
-                    res.out_lines.find(_.startsWith(SESSION_PARENT_PATH)).map(line =>
-                      line.substring(SESSION_PARENT_PATH.length))
+                    res.out_lines.find(_.startsWith(SESSION_PARENT_PATH))
+                      .map(_.substring(SESSION_PARENT_PATH.length))
                   else None
 
                 (parent_path, heap)
diff -r 1791a90a94fb -r a7aa17a1f721 src/Pure/Tools/ml_statistics.scala
--- a/src/Pure/Tools/ml_statistics.scala	Fri Jan 18 22:38:34 2013 +0100
+++ b/src/Pure/Tools/ml_statistics.scala	Fri Jan 18 23:33:17 2013 +0100
@@ -21,10 +21,13 @@
 
   final case class Entry(time: Double, data: Map[String, Double])
 
-  def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats)
-  def apply(path: Path): ML_Statistics = apply(Build.parse_log(File.read_gzip(path)).stats)
+  def apply(name: String, stats: List[Properties.T]): ML_Statistics =
+    new ML_Statistics(name, stats)
 
-  val empty = apply(Nil)
+  def apply(info: Build.Log_Info): ML_Statistics =
+    apply(info.name, info.stats)
+
+  val empty = apply("", Nil)
 
 
   /* standard fields */
@@ -53,7 +56,7 @@
     List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields)
 }
 
-final class ML_Statistics private(val stats: List[Properties.T])
+final class ML_Statistics private(val name: String, val stats: List[Properties.T])
 {
   val Now = new Properties.Double("now")
   def now(props: Properties.T): Double = Now.unapply(props).get
@@ -110,7 +113,7 @@
       Swing_Thread.later {
         new Frame {
           iconImage = Isabelle_System.get_icon().getImage
-          title = "Statistics"
+          title = name
           contents = Component.wrap(new ChartPanel(c))
           visible = true
         }
diff -r 1791a90a94fb -r a7aa17a1f721 src/Pure/Tools/task_statistics.scala
--- a/src/Pure/Tools/task_statistics.scala	Fri Jan 18 22:38:34 2013 +0100
+++ b/src/Pure/Tools/task_statistics.scala	Fri Jan 18 23:33:17 2013 +0100
@@ -17,18 +17,22 @@
 
 object Task_Statistics
 {
-  def apply(stats: List[Properties.T]): Task_Statistics = new Task_Statistics(stats)
+  def apply(name: String, tasks: List[Properties.T]): Task_Statistics =
+    new Task_Statistics(name, tasks)
+
+  def apply(info: Build.Log_Info): Task_Statistics =
+    apply(info.name, info.tasks)
 }
 
-final class Task_Statistics private(val stats: List[Properties.T])
+final class Task_Statistics private(val name: String, val tasks: List[Properties.T])
 {
-  val Task_Name = new Properties.String("task_name")
-  val Run = new Properties.Int("run")
+  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](stats.length)
-    for ((Run(x), i) <- stats.iterator.zipWithIndex) values(i) =
+    val values = new Array[Double](tasks.length)
+    for ((Run(x), i) <- tasks.iterator.zipWithIndex) values(i) =
       Math.log10(x.toDouble / 1000000)
 
     val data = new HistogramDataset
@@ -50,7 +54,7 @@
     Swing_Thread.later {
       new Frame {
         iconImage = Isabelle_System.get_icon().getImage
-        title = "Statistics"
+        title = name
         contents = Component.wrap(new ChartPanel(chart(bins)))
         visible = true
       }
diff -r 1791a90a94fb -r a7aa17a1f721 src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala	Fri Jan 18 22:38:34 2013 +0100
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Fri Jan 18 23:33:17 2013 +0100
@@ -28,7 +28,7 @@
 
   private val delay_update =
     Swing_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) {
-      ML_Statistics(rev_stats.reverse)
+      ML_Statistics("", rev_stats.reverse)
         .update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields
     }