# 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 \Miscellaneous tools\ -section \Timing\ +section \Timing and monitoring\ text \ Managed evaluation of commands within PIDE documents includes timing @@ -2103,13 +2103,19 @@ Isabelle~/ General\. \<^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>\Monitor\ panel for further details. + + \<^medskip> The \<^emph>\Monitor\ 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>\isabelle.ML_Statistics\ - provides further access to statistics of Isabelle/ML. + Isabelle/ML. \