--- a/NEWS Tue Aug 05 23:52:56 2014 +0200
+++ b/NEWS Fri Aug 08 11:43:08 2014 +0200
@@ -114,6 +114,8 @@
* Empty editors buffers that are no longer required (e.g.\ via theory
imports) are automatically removed from the document model.
+* Improved monitor panel.
+
* Improved Console/Scala plugin: more uniform scala.Console output,
more robust treatment of threads and interrupts.
--- a/src/Doc/JEdit/JEdit.thy Tue Aug 05 23:52:56 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy Fri Aug 08 11:43:08 2014 +0200
@@ -1595,14 +1595,14 @@
@{system_option_ref jedit_timing_threshold}, which can be configured in
\emph{Plugin Options~/ Isabelle~/ General}.
- \medskip The \emph{Monitor} panel provides a general impression of
- recent activity of the farm of worker threads in Isabelle/ML. Its
- display is continuously updated according to @{system_option_ref
- editor_chart_delay}. Note that the painting of the chart takes
- considerable runtime itself --- on the Java Virtual Machine that
- runs Isabelle/Scala, not Isabelle/ML. Internally, the
- Isabelle/Scala module @{verbatim isabelle.ML_Statistics} provides
- further access to statistics of Isabelle/ML. *}
+ \medskip The \emph{Monitor} panel visualizes various data collections about
+ recent activity of the Isabelle/ML task farm and the underlying ML runtime
+ system. The display is continuously updated according to @{system_option_ref
+ editor_chart_delay}. Note that the painting of the chart takes considerable
+ runtime itself --- on the Java Virtual Machine that runs Isabelle/Scala, not
+ Isabelle/ML. Internally, the Isabelle/Scala module @{verbatim
+ isabelle.ML_Statistics} provides further access to statistics of
+ Isabelle/ML. *}
section {* Low-level output *}
--- a/src/Pure/Tools/ml_statistics.scala Tue Aug 05 23:52:56 2014 +0200
+++ b/src/Pure/Tools/ml_statistics.scala Fri Aug 08 11:43:08 2014 +0200
@@ -33,6 +33,12 @@
/* standard fields */
+ val tasks_fields =
+ ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
+
+ val workers_fields =
+ ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
+
val GC_fields = ("GCs", List("partial_GCs", "full_GCs"))
val heap_fields =
@@ -47,15 +53,9 @@
val speed_fields = ("Speed", List("speed_CPU", "speed_GC"))
- val tasks_fields =
- ("Future tasks", List("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, speed_fields,
- tasks_fields, workers_fields)
+ List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields,
+ time_fields, speed_fields)
}
final class ML_Statistics private(val name: String, val stats: List[Properties.T])
--- a/src/Tools/jEdit/src/monitor_dockable.scala Tue Aug 05 23:52:56 2014 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Fri Aug 08 11:43:08 2014 +0200
@@ -1,7 +1,7 @@
/* Title: Tools/jEdit/src/monitor_dockable.scala
Author: Makarius
-Monitor for runtime statistics.
+Monitor for ML statistics.
*/
package isabelle.jedit
@@ -9,7 +9,10 @@
import isabelle._
-import scala.swing.{TextArea, ScrollPane, Component}
+import java.awt.BorderLayout
+
+import scala.swing.{TextArea, ScrollPane, Component, ComboBox, Button}
+import scala.swing.event.{SelectionChanged, ButtonClicked}
import org.jfree.chart.ChartPanel
import org.jfree.data.xy.XYSeriesCollection
@@ -24,16 +27,51 @@
/* chart data -- owned by GUI thread */
+ private var data_name = ML_Statistics.standard_fields(0)._1
private val chart = ML_Statistics.empty.chart(null, Nil)
private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
- private val delay_update =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) {
- ML_Statistics("", rev_stats.value.reverse)
- .update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields
+ private def update_chart: Unit =
+ ML_Statistics.standard_fields.find(_._1 == data_name) match {
+ case None =>
+ case Some((_, fields)) =>
+ ML_Statistics("", rev_stats.value.reverse).update_data(data, fields)
}
+ private val delay_update =
+ GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { update_chart }
+
+
+ /* controls */
+
+ private val select_data = new ComboBox[String](
+ ML_Statistics.standard_fields.map(_._1))
+ {
+ tooltip = "Select visualized data collection"
+ listenTo(selection)
+ reactions += {
+ case SelectionChanged(_) =>
+ data_name = selection.item
+ update_chart
+ }
+ }
+
+ val reset_data = new Button("Reset") {
+ tooltip = "Reset accumulated data"
+ reactions += {
+ case ButtonClicked(_) =>
+ rev_stats.change(_ => Nil)
+ update_chart
+ }
+ }
+
+ private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(select_data, reset_data)
+
+
+ /* layout */
+
set_content(new ChartPanel(chart))
+ add(controls.peer, BorderLayout.NORTH)
/* main */