--- a/src/Pure/Tools/ml_statistics.scala Sun Feb 26 22:01:54 2017 +0100
+++ b/src/Pure/Tools/ml_statistics.scala Sun Feb 26 22:13:07 2017 +0100
@@ -59,9 +59,13 @@
val speed_fields: Fields =
("Speed", List("speed_CPU", "speed_GC"))
- val standard_fields: List[Fields] =
+
+ val all_fields: List[Fields] =
List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields,
time_fields, speed_fields)
+
+ val main_fields: List[Fields] =
+ List(tasks_fields, workers_fields, heap_fields)
}
final class ML_Statistics private(val session_name: String, val ml_statistics: List[Properties.T])
@@ -136,7 +140,7 @@
def chart(fields: ML_Statistics.Fields): JFreeChart =
chart(fields._1, fields._2)
- def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.standard_fields): Unit =
+ def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit =
fields.map(chart(_)).foreach(c =>
GUI_Thread.later {
new Frame {
--- a/src/Tools/jEdit/src/monitor_dockable.scala Sun Feb 26 22:01:54 2017 +0100
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Sun Feb 26 22:13:07 2017 +0100
@@ -47,12 +47,12 @@
statistics_length = 0
}
- private var data_name = ML_Statistics.standard_fields(0)._1
+ private var data_name = ML_Statistics.all_fields(0)._1
private val chart = ML_Statistics.empty.chart(null, Nil)
private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
private def update_chart: Unit =
- ML_Statistics.standard_fields.find(_._1 == data_name) match {
+ ML_Statistics.all_fields.find(_._1 == data_name) match {
case None =>
case Some((_, fields)) => ML_Statistics("", statistics.toList).update_data(data, fields)
}
@@ -68,8 +68,7 @@
private val ml_stats = new Isabelle.ML_Stats
- private val select_data = new ComboBox[String](
- ML_Statistics.standard_fields.map(_._1))
+ private val select_data = new ComboBox[String](ML_Statistics.all_fields.map(_._1))
{
tooltip = "Select visualized data collection"
listenTo(selection)