improved monitor panel;
authorwenzelm
Fri Aug 08 11:43:08 2014 +0200 (2014-08-08)
changeset 578699665f79a7181
parent 57868 0b954ac94827
child 57870 561680651364
improved monitor panel;
NEWS
src/Doc/JEdit/JEdit.thy
src/Pure/Tools/ml_statistics.scala
src/Tools/jEdit/src/monitor_dockable.scala
     1.1 --- a/NEWS	Tue Aug 05 23:52:56 2014 +0200
     1.2 +++ b/NEWS	Fri Aug 08 11:43:08 2014 +0200
     1.3 @@ -114,6 +114,8 @@
     1.4  * Empty editors buffers that are no longer required (e.g.\ via theory
     1.5  imports) are automatically removed from the document model.
     1.6  
     1.7 +* Improved monitor panel.
     1.8 +
     1.9  * Improved Console/Scala plugin: more uniform scala.Console output,
    1.10  more robust treatment of threads and interrupts.
    1.11  
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Tue Aug 05 23:52:56 2014 +0200
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Fri Aug 08 11:43:08 2014 +0200
     2.3 @@ -1595,14 +1595,14 @@
     2.4    @{system_option_ref jedit_timing_threshold}, which can be configured in
     2.5    \emph{Plugin Options~/ Isabelle~/ General}.
     2.6  
     2.7 -  \medskip The \emph{Monitor} panel provides a general impression of
     2.8 -  recent activity of the farm of worker threads in Isabelle/ML.  Its
     2.9 -  display is continuously updated according to @{system_option_ref
    2.10 -  editor_chart_delay}.  Note that the painting of the chart takes
    2.11 -  considerable runtime itself --- on the Java Virtual Machine that
    2.12 -  runs Isabelle/Scala, not Isabelle/ML.  Internally, the
    2.13 -  Isabelle/Scala module @{verbatim isabelle.ML_Statistics} provides
    2.14 -  further access to statistics of Isabelle/ML.  *}
    2.15 +  \medskip The \emph{Monitor} panel visualizes various data collections about
    2.16 +  recent activity of the Isabelle/ML task farm and the underlying ML runtime
    2.17 +  system. The display is continuously updated according to @{system_option_ref
    2.18 +  editor_chart_delay}. Note that the painting of the chart takes considerable
    2.19 +  runtime itself --- on the Java Virtual Machine that runs Isabelle/Scala, not
    2.20 +  Isabelle/ML. Internally, the Isabelle/Scala module @{verbatim
    2.21 +  isabelle.ML_Statistics} provides further access to statistics of
    2.22 +  Isabelle/ML. *}
    2.23  
    2.24  
    2.25  section {* Low-level output *}
     3.1 --- a/src/Pure/Tools/ml_statistics.scala	Tue Aug 05 23:52:56 2014 +0200
     3.2 +++ b/src/Pure/Tools/ml_statistics.scala	Fri Aug 08 11:43:08 2014 +0200
     3.3 @@ -33,6 +33,12 @@
     3.4  
     3.5    /* standard fields */
     3.6  
     3.7 +  val tasks_fields =
     3.8 +    ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
     3.9 +
    3.10 +  val workers_fields =
    3.11 +    ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
    3.12 +
    3.13    val GC_fields = ("GCs", List("partial_GCs", "full_GCs"))
    3.14  
    3.15    val heap_fields =
    3.16 @@ -47,15 +53,9 @@
    3.17  
    3.18    val speed_fields = ("Speed", List("speed_CPU", "speed_GC"))
    3.19  
    3.20 -  val tasks_fields =
    3.21 -    ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
    3.22 -
    3.23 -  val workers_fields =
    3.24 -    ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
    3.25 -
    3.26    val standard_fields =
    3.27 -    List(GC_fields, heap_fields, threads_fields, time_fields, speed_fields,
    3.28 -      tasks_fields, workers_fields)
    3.29 +    List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields,
    3.30 +      time_fields, speed_fields)
    3.31  }
    3.32  
    3.33  final class ML_Statistics private(val name: String, val stats: List[Properties.T])
     4.1 --- a/src/Tools/jEdit/src/monitor_dockable.scala	Tue Aug 05 23:52:56 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/monitor_dockable.scala	Fri Aug 08 11:43:08 2014 +0200
     4.3 @@ -1,7 +1,7 @@
     4.4  /*  Title:      Tools/jEdit/src/monitor_dockable.scala
     4.5      Author:     Makarius
     4.6  
     4.7 -Monitor for runtime statistics.
     4.8 +Monitor for ML statistics.
     4.9  */
    4.10  
    4.11  package isabelle.jedit
    4.12 @@ -9,7 +9,10 @@
    4.13  
    4.14  import isabelle._
    4.15  
    4.16 -import scala.swing.{TextArea, ScrollPane, Component}
    4.17 +import java.awt.BorderLayout
    4.18 +
    4.19 +import scala.swing.{TextArea, ScrollPane, Component, ComboBox, Button}
    4.20 +import scala.swing.event.{SelectionChanged, ButtonClicked}
    4.21  
    4.22  import org.jfree.chart.ChartPanel
    4.23  import org.jfree.data.xy.XYSeriesCollection
    4.24 @@ -24,16 +27,51 @@
    4.25  
    4.26    /* chart data -- owned by GUI thread */
    4.27  
    4.28 +  private var data_name = ML_Statistics.standard_fields(0)._1
    4.29    private val chart = ML_Statistics.empty.chart(null, Nil)
    4.30    private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
    4.31  
    4.32 -  private val delay_update =
    4.33 -    GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) {
    4.34 -      ML_Statistics("", rev_stats.value.reverse)
    4.35 -        .update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields
    4.36 +  private def update_chart: Unit =
    4.37 +    ML_Statistics.standard_fields.find(_._1 == data_name) match {
    4.38 +      case None =>
    4.39 +      case Some((_, fields)) =>
    4.40 +        ML_Statistics("", rev_stats.value.reverse).update_data(data, fields)
    4.41      }
    4.42  
    4.43 +  private val delay_update =
    4.44 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { update_chart }
    4.45 +
    4.46 +
    4.47 +  /* controls */
    4.48 +
    4.49 +  private val select_data = new ComboBox[String](
    4.50 +    ML_Statistics.standard_fields.map(_._1))
    4.51 +  {
    4.52 +    tooltip = "Select visualized data collection"
    4.53 +    listenTo(selection)
    4.54 +    reactions += {
    4.55 +      case SelectionChanged(_) =>
    4.56 +        data_name = selection.item
    4.57 +        update_chart
    4.58 +    }
    4.59 +  }
    4.60 +
    4.61 +  val reset_data = new Button("Reset") {
    4.62 +    tooltip = "Reset accumulated data"
    4.63 +    reactions += {
    4.64 +      case ButtonClicked(_) =>
    4.65 +        rev_stats.change(_ => Nil)
    4.66 +        update_chart
    4.67 +    }
    4.68 +  }
    4.69 +
    4.70 +  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(select_data, reset_data)
    4.71 +
    4.72 +
    4.73 +  /* layout */
    4.74 +
    4.75    set_content(new ChartPanel(chart))
    4.76 +  add(controls.peer, BorderLayout.NORTH)
    4.77  
    4.78  
    4.79    /* main */