# HG changeset patch
# User wenzelm
# Date 1355001564 -3600
# Node ID 9131dadb2bf7e1bd26f3224596c5014801f34b1d
# Parent f9d70f49d3700104c9f1fb2aa02d2fa41a2a2105
basic monitor panel, using the powerful jfreechart library;
sorted Isabelle menu entries -- this is mainly a catalog;
diff -r f9d70f49d370 -r 9131dadb2bf7 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala Sat Dec 08 22:14:39 2012 +0100
+++ b/src/Pure/System/session.scala Sat Dec 08 22:19:24 2012 +0100
@@ -22,6 +22,7 @@
/* events */
//{{{
+ case class Statistics(stats: Properties.T)
case class Global_Options(options: Options)
case object Caret_Focus
case class Raw_Edits(edits: List[Document.Edit_Text])
@@ -58,6 +59,7 @@
/* pervasive event buses */
+ val statistics = new Event_Bus[Session.Statistics]
val global_options = new Event_Bus[Session.Global_Options]
val caret_focus = new Event_Bus[Session.Caret_Focus.type]
val raw_edits = new Event_Bus[Session.Raw_Edits]
@@ -359,10 +361,10 @@
}
case Markup.ML_Statistics(stats) if output.is_protocol =>
- java.lang.System.err.println(stats.toString) // FIXME
+ statistics.event(Session.Statistics(stats))
case _ if output.is_init =>
- phase = Session.Ready
+ phase = Session.Ready
case Markup.Return_Code(rc) if output.is_exit =>
if (rc == 0) phase = Session.Inactive
diff -r f9d70f49d370 -r 9131dadb2bf7 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit Sat Dec 08 22:14:39 2012 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Sat Dec 08 22:19:24 2012 +0100
@@ -24,6 +24,7 @@
"src/jedit_main.scala"
"src/jedit_options.scala"
"src/jedit_thy_load.scala"
+ "src/monitor_dockable.scala"
"src/output_dockable.scala"
"src/plugin.scala"
"src/pretty_text_area.scala"
@@ -204,6 +205,12 @@
"$ISABELLE_JEDIT_BUILD_HOME/contrib/js.jar"
)
+declare -a JFREECHART_JARS=()
+for NAME in $JFREECHART_JAR_NAMES
+do
+ JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$JFREECHART_HOME/lib/$NAME"
+done
+
# target
@@ -220,7 +227,7 @@
else
if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
declare -a DEPS=(
- "$JEDIT_JAR" "${JEDIT_JARS[@]}"
+ "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}"
"$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}"
)
elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
@@ -276,8 +283,8 @@
cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
(
- for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR" \
- "$SCALA_HOME/lib/scala-compiler.jar"
+ for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}" "$PURE_JAR" \
+ "$GRAPHVIEW_JAR" "$SCALA_HOME/lib/scala-compiler.jar"
do
CLASSPATH="$CLASSPATH:$JAR"
done
diff -r f9d70f49d370 -r 9131dadb2bf7 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props Sat Dec 08 22:14:39 2012 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props Sat Dec 08 22:19:24 2012 +0100
@@ -28,26 +28,37 @@
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.theories-panel isabelle.output-panel isabelle.graphview-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.symbols-panel isabelle.syslog-panel
-isabelle.theories-panel.label=Theories panel
+plugin.isabelle.jedit.Plugin.menu= \
+ isabelle.graphview-panel \
+ isabelle.monitor-panel \
+ isabelle.output-panel \
+ isabelle.protocol-panel \
+ isabelle.raw-output-panel \
+ isabelle.readme-panel \
+ isabelle.symbols-panel \
+ isabelle.syslog-panel \
+ isabelle.theories-panel
+isabelle.graphview-panel.label=Graphview panel
+isabelle.monitor-panel.label=Monitor panel
isabelle.output-panel.label=Output panel
-isabelle.graphview-panel.label=Graphview panel
+isabelle.protocol-panel.label=Protocol panel
isabelle.raw-output-panel.label=Raw Output panel
-isabelle.protocol-panel.label=Protocol panel
isabelle.readme-panel.label=README panel
isabelle.symbols-panel.label=Symbols panel
isabelle.syslog-panel.label=Syslog panel
+isabelle.theories-panel.label=Theories panel
#dockables
-isabelle-theories.title=Theories
+isabelle-graphview.title=Graphview
+isabelle-info.title=Info
+isabelle-monitor.title=Monitor
isabelle-output.title=Output
-isabelle-info.title=Info
-isabelle-graphview.title=Graphview
+isabelle-protocol.title=Protocol
isabelle-raw-output.title=Raw Output
-isabelle-protocol.title=Protocol
isabelle-readme.title=README
+isabelle-symbols.title=Symbols
isabelle-syslog.title=Syslog
-isabelle-symbols.title=Symbols
+isabelle-theories.title=Theories
#SideKick
mode.isabelle-options.folding=sidekick
diff -r f9d70f49d370 -r 9131dadb2bf7 src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml Sat Dec 08 22:14:39 2012 +0100
+++ b/src/Tools/jEdit/src/actions.xml Sat Dec 08 22:19:24 2012 +0100
@@ -37,6 +37,11 @@
wm.addDockableWindow("isabelle-protocol");
+
+
+ wm.addDockableWindow("isabelle-monitor");
+
+
wm.addDockableWindow("isabelle-symbols");
diff -r f9d70f49d370 -r 9131dadb2bf7 src/Tools/jEdit/src/dockables.xml
--- a/src/Tools/jEdit/src/dockables.xml Sat Dec 08 22:14:39 2012 +0100
+++ b/src/Tools/jEdit/src/dockables.xml Sat Dec 08 22:19:24 2012 +0100
@@ -26,6 +26,9 @@
new isabelle.jedit.Protocol_Dockable(view, position);
+
+ new isabelle.jedit.Monitor_Dockable(view, position);
+
new isabelle.jedit.Symbols_Dockable(view, position);
diff -r f9d70f49d370 -r 9131dadb2bf7 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala Sat Dec 08 22:14:39 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Sat Dec 08 22:19:24 2012 +0100
@@ -44,6 +44,12 @@
case _ => None
}
+ def docked_monitor(view: View): Option[Monitor_Dockable] =
+ wm(view).getDockableWindow("isabelle-monitor") match {
+ case dockable: Monitor_Dockable => Some(dockable)
+ case _ => None
+ }
+
/* font size */
diff -r f9d70f49d370 -r 9131dadb2bf7 src/Tools/jEdit/src/monitor_dockable.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Sat Dec 08 22:19:24 2012 +0100
@@ -0,0 +1,77 @@
+/* Title: Tools/jEdit/src/monitor_dockable.scala
+ Author: Makarius
+
+Monitor for runtime statistics.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.actors.Actor._
+import scala.swing.{TextArea, ScrollPane, Component}
+
+import org.jfree.chart.{ChartFactory, ChartPanel}
+import org.jfree.data.time.{Millisecond, TimeSeries, TimeSeriesCollection}
+
+import org.gjt.sp.jedit.View
+
+
+class Monitor_Dockable(view: View, position: String) extends Dockable(view, position)
+{
+ /* properties */ // FIXME avoid hardwired stuff
+
+ private val Now = new Properties.Double("now")
+ private val Size_Heap = new Properties.Double("size_heap")
+
+ private val series = new TimeSeries("ML heap size", classOf[Millisecond])
+
+
+ /* chart */
+
+ private val chart_panel =
+ {
+ val data = new TimeSeriesCollection(series)
+ val chart = ChartFactory.createTimeSeriesChart(null, "Time", "Value", data, true, true, false)
+ val plot = chart.getXYPlot()
+
+ val x_axis = plot.getDomainAxis()
+ x_axis.setAutoRange(true)
+ x_axis.setFixedAutoRange(60000.0)
+
+ val y_axis = plot.getRangeAxis()
+ y_axis.setAutoRange(true)
+
+ new ChartPanel(chart)
+ }
+ set_content(chart_panel)
+
+
+ /* main actor */
+
+ private val main_actor = actor {
+ var t0: Option[Double] = None
+ loop {
+ react {
+ case Session.Statistics(stats) =>
+ java.lang.System.err.println(stats)
+ stats match {
+ case Now(t1) =>
+ if (t0.isEmpty) t0 = Some(t1)
+ val t = t1 - t0.get
+ stats match {
+ case Size_Heap(x) => series.add(new Millisecond(), x) // FIXME proper time point
+ case _ =>
+ }
+ case _ =>
+ }
+ case bad => java.lang.System.err.println("Monitor_Dockable: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ override def init() { PIDE.session.statistics += main_actor }
+ override def exit() { PIDE.session.statistics -= main_actor }
+}
+