# HG changeset patch
# User wenzelm
# Date 1407490988 -7200
# Node ID 9665f79a718151f61d502a6c11f7273df1cf1ad9
# Parent  0b954ac948272dc3b1e02cefa48ef659c8a443ac
improved monitor panel;

diff -r 0b954ac94827 -r 9665f79a7181 NEWS
--- 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.
 
diff -r 0b954ac94827 -r 9665f79a7181 src/Doc/JEdit/JEdit.thy
--- 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 *}
diff -r 0b954ac94827 -r 9665f79a7181 src/Pure/Tools/ml_statistics.scala
--- 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])
diff -r 0b954ac94827 -r 9665f79a7181 src/Tools/jEdit/src/monitor_dockable.scala
--- 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 */