# HG changeset patch
# User wenzelm
# Date 1597326760 -7200
# Node ID 510ebf84669673eedab1bdfb40518992d3e7bd58
# Parent  36a34f3a8cb80bbadbe35e8e14148920ff82a672
more documentation;

diff -r 36a34f3a8cb8 -r 510ebf846696 CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Aug 13 15:11:30 2020 +0200
+++ b/CONTRIBUTORS	Thu Aug 13 15:52:40 2020 +0200
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* August 2020: Makarius Wenzel
+  Improved monitoring of runtime statistics: ML GC progress and Java.
+
 * July 2020: Martin Desharnais
   Integration of Metis 2.4.
 
diff -r 36a34f3a8cb8 -r 510ebf846696 NEWS
--- a/NEWS	Thu Aug 13 15:11:30 2020 +0200
+++ b/NEWS	Thu Aug 13 15:52:40 2020 +0200
@@ -9,6 +9,14 @@
 
 *** Isabelle/jEdit Prover IDE ***
 
+* The jEdit status line includes a widget for Isabelle/ML heap usage,
+including an indication for ongoing garbage collection (as "ML
+cleanup").
+
+* The Monitor dockable provides buttons to request a full garbage
+collection and sharing of live data on the ML heap. It also includes
+information about the Java Runtime system.
+
 * Update to jedit-5.6pre1, the latest pre-release. This version works
 properly on macOS by default, without the special MacOSX plugin.
 
diff -r 36a34f3a8cb8 -r 510ebf846696 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Thu Aug 13 15:11:30 2020 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Thu Aug 13 15:52:40 2020 +0200
@@ -2077,7 +2077,7 @@
 
 chapter \<open>Miscellaneous tools\<close>
 
-section \<open>Timing\<close>
+section \<open>Timing and monitoring\<close>
 
 text \<open>
   Managed evaluation of commands within PIDE documents includes timing
@@ -2103,13 +2103,19 @@
   Isabelle~/ General\<close>.
 
   \<^medskip>
+  The jEdit status line includes monitor widgets for current heap usage of
+  Java and Isabelle/ML, respectively. The one for ML includes information
+  about ongoing garbage collection (as ``ML cleanup''); a double-click opens
+  a new instance of the \<^emph>\<open>Monitor\<close> panel for further details.
+
+  \<^medskip>
   The \<^emph>\<open>Monitor\<close> panel visualizes various data collections about recent
-  activity of the Isabelle/ML task farm and the underlying ML runtime system.
+  activity of the runtime system of Isabelle/ML and Java. There are buttons to
+  request a full garbage collection and sharing of live data on the ML heap.
   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>\<open>isabelle.ML_Statistics\<close>
-  provides further access to statistics of Isabelle/ML.
+  Isabelle/ML.
 \<close>