# HG changeset patch
# User wenzelm
# Date 1383493074 -3600
# Node ID 9d19298d36508d83e7b382f86af8cb9c1e6eee8c
# Parent  e649dff217ae446d0507465b4a9f53d21cad3ae5
more on Monitor panel;

diff -r e649dff217ae -r 9d19298d3650 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sun Nov 03 16:22:57 2013 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sun Nov 03 16:37:54 2013 +0100
@@ -877,7 +877,16 @@
   modifier key as explained in \secref{sec:tooltips-hyperlinks}.
   Actual display of timing depends on the global option
   @{system_option jedit_timing_threshold}, which can be configured in
-  "Plugin Options / Isabelle / General".  *}
+  "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
+  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 runtime statistics of Isabelle/ML.  *}
 
 
 section {* Isabelle/Scala console *}