use inlined session name as title for charts;
authorwenzelm
Fri Jan 18 23:33:17 2013 +0100 (2013-01-18 ago)
changeset 50982a7aa17a1f721
parent 50981 1791a90a94fb
child 50983 1290afb88f90
use inlined session name as title for charts;
tuned signature;
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
src/Pure/Tools/ml_statistics.scala
src/Pure/Tools/task_statistics.scala
src/Tools/jEdit/src/monitor_dockable.scala
     1.1 --- a/src/Pure/Tools/build.ML	Fri Jan 18 22:38:34 2013 +0100
     1.2 +++ b/src/Pure/Tools/build.ML	Fri Jan 18 23:33:17 2013 +0100
     1.3 @@ -98,6 +98,7 @@
     1.4            [] => ()
     1.5          | dups => error ("Duplicate document variants: " ^ commas_quote dups));
     1.6  
     1.7 +      val _ = writeln ("\fSession.name = " ^ name);
     1.8        val _ =
     1.9          (case Session.path () of
    1.10            [] => ()
     2.1 --- a/src/Pure/Tools/build.scala	Fri Jan 18 22:38:34 2013 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Fri Jan 18 23:33:17 2013 +0100
     2.3 @@ -558,19 +558,22 @@
     2.4    private def log(name: String): Path = LOG + Path.basic(name)
     2.5    private def log_gz(name: String): Path = log(name).ext("gz")
     2.6  
     2.7 +  private val SESSION_NAME = "\fSession.name = "
     2.8    private val SESSION_PARENT_PATH = "\fSession.parent_path = "
     2.9  
    2.10  
    2.11    sealed case class Log_Info(
    2.12 -    stats: List[Properties.T], tasks: List[Properties.T], timing: Properties.T)
    2.13 +    name: String, stats: List[Properties.T], tasks: List[Properties.T], timing: Properties.T)
    2.14  
    2.15    def parse_log(text: String): Log_Info =
    2.16    {
    2.17      val lines = split_lines(text)
    2.18 +    val name =
    2.19 +      lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) getOrElse ""
    2.20      val stats = Props.parse_lines("\fML_statistics = ", lines)
    2.21      val tasks = Props.parse_lines("\ftask_statistics = ", lines)
    2.22      val timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
    2.23 -    Log_Info(stats, tasks, timing)
    2.24 +    Log_Info(name, stats, tasks, timing)
    2.25    }
    2.26  
    2.27  
    2.28 @@ -694,8 +697,8 @@
    2.29  
    2.30                  val parent_path =
    2.31                    if (job.info.options.bool("browser_info"))
    2.32 -                    res.out_lines.find(_.startsWith(SESSION_PARENT_PATH)).map(line =>
    2.33 -                      line.substring(SESSION_PARENT_PATH.length))
    2.34 +                    res.out_lines.find(_.startsWith(SESSION_PARENT_PATH))
    2.35 +                      .map(_.substring(SESSION_PARENT_PATH.length))
    2.36                    else None
    2.37  
    2.38                  (parent_path, heap)
     3.1 --- a/src/Pure/Tools/ml_statistics.scala	Fri Jan 18 22:38:34 2013 +0100
     3.2 +++ b/src/Pure/Tools/ml_statistics.scala	Fri Jan 18 23:33:17 2013 +0100
     3.3 @@ -21,10 +21,13 @@
     3.4  
     3.5    final case class Entry(time: Double, data: Map[String, Double])
     3.6  
     3.7 -  def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats)
     3.8 -  def apply(path: Path): ML_Statistics = apply(Build.parse_log(File.read_gzip(path)).stats)
     3.9 +  def apply(name: String, stats: List[Properties.T]): ML_Statistics =
    3.10 +    new ML_Statistics(name, stats)
    3.11  
    3.12 -  val empty = apply(Nil)
    3.13 +  def apply(info: Build.Log_Info): ML_Statistics =
    3.14 +    apply(info.name, info.stats)
    3.15 +
    3.16 +  val empty = apply("", Nil)
    3.17  
    3.18  
    3.19    /* standard fields */
    3.20 @@ -53,7 +56,7 @@
    3.21      List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields)
    3.22  }
    3.23  
    3.24 -final class ML_Statistics private(val stats: List[Properties.T])
    3.25 +final class ML_Statistics private(val name: String, val stats: List[Properties.T])
    3.26  {
    3.27    val Now = new Properties.Double("now")
    3.28    def now(props: Properties.T): Double = Now.unapply(props).get
    3.29 @@ -110,7 +113,7 @@
    3.30        Swing_Thread.later {
    3.31          new Frame {
    3.32            iconImage = Isabelle_System.get_icon().getImage
    3.33 -          title = "Statistics"
    3.34 +          title = name
    3.35            contents = Component.wrap(new ChartPanel(c))
    3.36            visible = true
    3.37          }
     4.1 --- a/src/Pure/Tools/task_statistics.scala	Fri Jan 18 22:38:34 2013 +0100
     4.2 +++ b/src/Pure/Tools/task_statistics.scala	Fri Jan 18 23:33:17 2013 +0100
     4.3 @@ -17,18 +17,22 @@
     4.4  
     4.5  object Task_Statistics
     4.6  {
     4.7 -  def apply(stats: List[Properties.T]): Task_Statistics = new Task_Statistics(stats)
     4.8 +  def apply(name: String, tasks: List[Properties.T]): Task_Statistics =
     4.9 +    new Task_Statistics(name, tasks)
    4.10 +
    4.11 +  def apply(info: Build.Log_Info): Task_Statistics =
    4.12 +    apply(info.name, info.tasks)
    4.13  }
    4.14  
    4.15 -final class Task_Statistics private(val stats: List[Properties.T])
    4.16 +final class Task_Statistics private(val name: String, val tasks: List[Properties.T])
    4.17  {
    4.18 -  val Task_Name = new Properties.String("task_name")
    4.19 -  val Run = new Properties.Int("run")
    4.20 +  private val Task_Name = new Properties.String("task_name")
    4.21 +  private val Run = new Properties.Int("run")
    4.22  
    4.23    def chart(bins: Int = 100): JFreeChart =
    4.24    {
    4.25 -    val values = new Array[Double](stats.length)
    4.26 -    for ((Run(x), i) <- stats.iterator.zipWithIndex) values(i) =
    4.27 +    val values = new Array[Double](tasks.length)
    4.28 +    for ((Run(x), i) <- tasks.iterator.zipWithIndex) values(i) =
    4.29        Math.log10(x.toDouble / 1000000)
    4.30  
    4.31      val data = new HistogramDataset
    4.32 @@ -50,7 +54,7 @@
    4.33      Swing_Thread.later {
    4.34        new Frame {
    4.35          iconImage = Isabelle_System.get_icon().getImage
    4.36 -        title = "Statistics"
    4.37 +        title = name
    4.38          contents = Component.wrap(new ChartPanel(chart(bins)))
    4.39          visible = true
    4.40        }
     5.1 --- a/src/Tools/jEdit/src/monitor_dockable.scala	Fri Jan 18 22:38:34 2013 +0100
     5.2 +++ b/src/Tools/jEdit/src/monitor_dockable.scala	Fri Jan 18 23:33:17 2013 +0100
     5.3 @@ -28,7 +28,7 @@
     5.4  
     5.5    private val delay_update =
     5.6      Swing_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) {
     5.7 -      ML_Statistics(rev_stats.reverse)
     5.8 +      ML_Statistics("", rev_stats.reverse)
     5.9          .update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields
    5.10      }
    5.11