--- a/src/Pure/ML/ml_statistics.scala Fri Jan 18 22:31:57 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,119 +0,0 @@
-/* Title: Pure/ML/ml_statistics.ML
- Author: Makarius
-
-ML runtime statistics.
-*/
-
-package isabelle
-
-
-import scala.collection.immutable.{SortedSet, SortedMap}
-import scala.swing.{Frame, Component}
-
-import org.jfree.data.xy.{XYSeries, XYSeriesCollection}
-import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
-import org.jfree.chart.plot.PlotOrientation
-
-
-object ML_Statistics
-{
- /* content interpretation */
-
- 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)
-
- val empty = apply(Nil)
-
-
- /* standard fields */
-
- val GC_fields = ("GCs", List("partial_GCs", "full_GCs"))
-
- val heap_fields =
- ("Heap", List("size_heap", "size_allocation", "size_allocation_free",
- "size_heap_free_last_full_GC", "size_heap_free_last_GC"))
-
- val threads_fields =
- ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
- "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
-
- val time_fields =
- ("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user"))
-
- val tasks_fields =
- ("Future tasks",
- List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
-
- val workers_fields =
- ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
-
- val standard_fields =
- List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields)
-}
-
-final class ML_Statistics private(val stats: List[Properties.T])
-{
- val Now = new Properties.Double("now")
- def now(props: Properties.T): Double = Now.unapply(props).get
-
- require(stats.forall(props => Now.unapply(props).isDefined))
-
- val time_start = if (stats.isEmpty) 0.0 else now(stats.head)
- val duration = if (stats.isEmpty) 0.0 else now(stats.last) - time_start
-
- val fields: Set[String] =
- SortedSet.empty[String] ++
- (for (props <- stats.iterator; (x, _) <- props.iterator if x != Now.name)
- yield x)
-
- val content: List[ML_Statistics.Entry] =
- stats.map(props => {
- val time = now(props) - time_start
- require(time >= 0.0)
- val data =
- SortedMap.empty[String, Double] ++
- (for ((x, y) <- props.iterator if x != Now.name)
- yield (x, java.lang.Double.parseDouble(y)))
- ML_Statistics.Entry(time, data)
- })
-
-
- /* charts */
-
- def update_data(data: XYSeriesCollection, selected_fields: Iterable[String])
- {
- data.removeAllSeries
- for {
- field <- selected_fields.iterator
- series = new XYSeries(field)
- } {
- content.foreach(entry => series.add(entry.time, entry.data(field)))
- data.addSeries(series)
- }
- }
-
- def chart(title: String, selected_fields: Iterable[String]): JFreeChart =
- {
- val data = new XYSeriesCollection
- update_data(data, selected_fields)
-
- ChartFactory.createXYLineChart(title, "time", "value", data,
- PlotOrientation.VERTICAL, true, true, true)
- }
-
- def chart(arg: (String, Iterable[String])): JFreeChart = chart(arg._1, arg._2)
-
- def standard_frames: Unit =
- ML_Statistics.standard_fields.map(chart(_)).foreach(c =>
- Swing_Thread.later {
- new Frame {
- iconImage = Isabelle_System.get_icon().getImage
- title = "ML statistics"
- contents = Component.wrap(new ChartPanel(c))
- visible = true
- }
- })
-}
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/ml_statistics.scala Fri Jan 18 22:38:34 2013 +0100
@@ -0,0 +1,119 @@
+/* Title: Pure/ML/ml_statistics.ML
+ Author: Makarius
+
+ML runtime statistics.
+*/
+
+package isabelle
+
+
+import scala.collection.immutable.{SortedSet, SortedMap}
+import scala.swing.{Frame, Component}
+
+import org.jfree.data.xy.{XYSeries, XYSeriesCollection}
+import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
+import org.jfree.chart.plot.PlotOrientation
+
+
+object ML_Statistics
+{
+ /* content interpretation */
+
+ 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)
+
+ val empty = apply(Nil)
+
+
+ /* standard fields */
+
+ val GC_fields = ("GCs", List("partial_GCs", "full_GCs"))
+
+ val heap_fields =
+ ("Heap", List("size_heap", "size_allocation", "size_allocation_free",
+ "size_heap_free_last_full_GC", "size_heap_free_last_GC"))
+
+ val threads_fields =
+ ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
+ "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
+
+ val time_fields =
+ ("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user"))
+
+ val tasks_fields =
+ ("Future tasks",
+ List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
+
+ val workers_fields =
+ ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
+
+ val standard_fields =
+ List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields)
+}
+
+final class ML_Statistics private(val stats: List[Properties.T])
+{
+ val Now = new Properties.Double("now")
+ def now(props: Properties.T): Double = Now.unapply(props).get
+
+ require(stats.forall(props => Now.unapply(props).isDefined))
+
+ val time_start = if (stats.isEmpty) 0.0 else now(stats.head)
+ val duration = if (stats.isEmpty) 0.0 else now(stats.last) - time_start
+
+ val fields: Set[String] =
+ SortedSet.empty[String] ++
+ (for (props <- stats.iterator; (x, _) <- props.iterator if x != Now.name)
+ yield x)
+
+ val content: List[ML_Statistics.Entry] =
+ stats.map(props => {
+ val time = now(props) - time_start
+ require(time >= 0.0)
+ val data =
+ SortedMap.empty[String, Double] ++
+ (for ((x, y) <- props.iterator if x != Now.name)
+ yield (x, java.lang.Double.parseDouble(y)))
+ ML_Statistics.Entry(time, data)
+ })
+
+
+ /* charts */
+
+ def update_data(data: XYSeriesCollection, selected_fields: Iterable[String])
+ {
+ data.removeAllSeries
+ for {
+ field <- selected_fields.iterator
+ series = new XYSeries(field)
+ } {
+ content.foreach(entry => series.add(entry.time, entry.data(field)))
+ data.addSeries(series)
+ }
+ }
+
+ def chart(title: String, selected_fields: Iterable[String]): JFreeChart =
+ {
+ val data = new XYSeriesCollection
+ update_data(data, selected_fields)
+
+ ChartFactory.createXYLineChart(title, "time", "value", data,
+ PlotOrientation.VERTICAL, true, true, true)
+ }
+
+ def chart(arg: (String, Iterable[String])): JFreeChart = chart(arg._1, arg._2)
+
+ def show_standard_frames(): Unit =
+ ML_Statistics.standard_fields.map(chart(_)).foreach(c =>
+ Swing_Thread.later {
+ new Frame {
+ iconImage = Isabelle_System.get_icon().getImage
+ title = "Statistics"
+ contents = Component.wrap(new ChartPanel(c))
+ visible = true
+ }
+ })
+}
+
--- a/src/Pure/build-jars Fri Jan 18 22:31:57 2013 +0100
+++ b/src/Pure/build-jars Fri Jan 18 22:38:34 2013 +0100
@@ -30,7 +30,6 @@
Isar/outer_syntax.scala
Isar/parse.scala
Isar/token.scala
- ML/ml_statistics.scala
PIDE/command.scala
PIDE/document.scala
PIDE/markup.scala
@@ -65,6 +64,7 @@
Tools/build.scala
Tools/build_dialog.scala
Tools/main.scala
+ Tools/ml_statistics.scala
Tools/task_statistics.scala
library.scala
package.scala