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