clarified defaults;
authorwenzelm
Sun Feb 26 22:13:07 2017 +0100 (2017-02-26 ago)
changeset 65053460f0fd2f77a
parent 65052 7f825cc6debf
child 65054 9ad3f65c03f4
clarified defaults;
src/Pure/Tools/ml_statistics.scala
src/Tools/jEdit/src/monitor_dockable.scala
     1.1 --- a/src/Pure/Tools/ml_statistics.scala	Sun Feb 26 22:01:54 2017 +0100
     1.2 +++ b/src/Pure/Tools/ml_statistics.scala	Sun Feb 26 22:13:07 2017 +0100
     1.3 @@ -59,9 +59,13 @@
     1.4    val speed_fields: Fields =
     1.5      ("Speed", List("speed_CPU", "speed_GC"))
     1.6  
     1.7 -  val standard_fields: List[Fields] =
     1.8 +
     1.9 +  val all_fields: List[Fields] =
    1.10      List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields,
    1.11        time_fields, speed_fields)
    1.12 +
    1.13 +  val main_fields: List[Fields] =
    1.14 +    List(tasks_fields, workers_fields, heap_fields)
    1.15  }
    1.16  
    1.17  final class ML_Statistics private(val session_name: String, val ml_statistics: List[Properties.T])
    1.18 @@ -136,7 +140,7 @@
    1.19    def chart(fields: ML_Statistics.Fields): JFreeChart =
    1.20      chart(fields._1, fields._2)
    1.21  
    1.22 -  def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.standard_fields): Unit =
    1.23 +  def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit =
    1.24      fields.map(chart(_)).foreach(c =>
    1.25        GUI_Thread.later {
    1.26          new Frame {
     2.1 --- a/src/Tools/jEdit/src/monitor_dockable.scala	Sun Feb 26 22:01:54 2017 +0100
     2.2 +++ b/src/Tools/jEdit/src/monitor_dockable.scala	Sun Feb 26 22:13:07 2017 +0100
     2.3 @@ -47,12 +47,12 @@
     2.4      statistics_length = 0
     2.5    }
     2.6  
     2.7 -  private var data_name = ML_Statistics.standard_fields(0)._1
     2.8 +  private var data_name = ML_Statistics.all_fields(0)._1
     2.9    private val chart = ML_Statistics.empty.chart(null, Nil)
    2.10    private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
    2.11  
    2.12    private def update_chart: Unit =
    2.13 -    ML_Statistics.standard_fields.find(_._1 == data_name) match {
    2.14 +    ML_Statistics.all_fields.find(_._1 == data_name) match {
    2.15        case None =>
    2.16        case Some((_, fields)) => ML_Statistics("", statistics.toList).update_data(data, fields)
    2.17      }
    2.18 @@ -68,8 +68,7 @@
    2.19  
    2.20    private val ml_stats = new Isabelle.ML_Stats
    2.21  
    2.22 -  private val select_data = new ComboBox[String](
    2.23 -    ML_Statistics.standard_fields.map(_._1))
    2.24 +  private val select_data = new ComboBox[String](ML_Statistics.all_fields.map(_._1))
    2.25    {
    2.26      tooltip = "Select visualized data collection"
    2.27      listenTo(selection)