basic monitor panel, using the powerful jfreechart library;
sorted Isabelle menu entries -- this is mainly a catalog;

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

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

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

--- 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");
 		</CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.monitor-panel">
+		<CODE>
+			wm.addDockableWindow("isabelle-monitor");
+		</CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.symbols-panel">
 		<CODE>
 			wm.addDockableWindow("isabelle-symbols");

--- 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 @@
 	<DOCKABLE NAME="isabelle-protocol" MOVABLE="TRUE">
 		new isabelle.jedit.Protocol_Dockable(view, position);
 	</DOCKABLE>
+	<DOCKABLE NAME="isabelle-monitor" MOVABLE="TRUE">
+		new isabelle.jedit.Monitor_Dockable(view, position);
+	</DOCKABLE>
 	<DOCKABLE NAME="isabelle-symbols" MOVABLE="TRUE">
 		new isabelle.jedit.Symbols_Dockable(view, position);
 	</DOCKABLE>

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

--- /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 }
+}
+