# HG changeset patch
# User wenzelm
# Date 1488143587 -3600
# Node ID 460f0fd2f77a5e3acddd7640ff4931ae7b1c53e8
# Parent  7f825cc6debf0805a235517d009d807b65ffc185
clarified defaults;

diff -r 7f825cc6debf -r 460f0fd2f77a src/Pure/Tools/ml_statistics.scala
--- 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 {
diff -r 7f825cc6debf -r 460f0fd2f77a src/Tools/jEdit/src/monitor_dockable.scala
--- 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)