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 */