more uniform JVM vs. ML status widget;
--- a/NEWS Thu Sep 10 16:04:12 2020 +0200
+++ b/NEWS Thu Sep 10 21:07:58 2020 +0200
@@ -16,9 +16,8 @@
*** 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 jEdit status line includes widgets both for JVM and ML heap usage.
+Ongoing ML ongoing garbage collection is shown 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
--- a/src/Doc/JEdit/JEdit.thy Thu Sep 10 16:04:12 2020 +0200
+++ b/src/Doc/JEdit/JEdit.thy Thu Sep 10 21:07:58 2020 +0200
@@ -2103,10 +2103,11 @@
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.
+ The jEdit status line includes monitor widgets for current heap usage of the
+ Java VM and Isabelle/ML, respectively. The one for ML includes information
+ about ongoing garbage collection (as ``ML cleanup''). For further details, a
+ double-clicking the JVM widget opens the external \<^verbatim>\<open>jconsole\<close> application,
+ and the ML widget a new instance of the \<^emph>\<open>Monitor\<close> panel.
\<^medskip>
The \<^emph>\<open>Monitor\<close> panel visualizes various data collections about recent
--- a/src/Pure/System/platform.scala Thu Sep 10 16:04:12 2020 +0200
+++ b/src/Pure/System/platform.scala Thu Sep 10 21:07:58 2020 +0200
@@ -70,20 +70,35 @@
val jvm_name: String = System.getProperty("java.vm.name", "")
+ /* memory status */
+
+ sealed case class Memory_Status(heap_size: Long, heap_free: Long)
+ {
+ def heap_used: Long = (heap_size - heap_free) max 0
+ def heap_used_fraction: Double =
+ if (heap_size == 0) 0.0 else heap_used.toDouble / heap_size
+ }
+
+ def memory_status(): Memory_Status =
+ {
+ val heap_size = Runtime.getRuntime.totalMemory()
+ val heap_used = heap_size - Runtime.getRuntime.freeMemory()
+ Memory_Status(heap_size, heap_used)
+ }
+
+
/* JVM statistics */
def jvm_statistics(): Properties.T =
{
- val heap_size = Runtime.getRuntime.totalMemory()
- val heap_used = heap_size - Runtime.getRuntime.freeMemory()
-
+ val status = memory_status()
val threads = Thread.activeCount()
val workers = Isabelle_Thread.pool.getPoolSize
val workers_active = Isabelle_Thread.pool.getActiveCount
List(
- "java_heap_size" -> heap_size.toString,
- "java_heap_used" -> heap_used.toString,
+ "java_heap_size" -> status.heap_size.toString,
+ "java_heap_used" -> status.heap_used.toString,
"java_threads_total" -> threads.toString,
"java_workers_total" -> workers.toString,
"java_workers_active" -> workers_active.toString)
--- a/src/Tools/jEdit/src/jEdit.props Thu Sep 10 16:04:12 2020 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Thu Sep 10 21:07:58 2020 +0200
@@ -337,7 +337,7 @@
view.height=850
view.middleMousePaste=true
view.showToolbar=true
-view.status=( mode , fold , encoding ) locked wrap multiSelect rectSelect overwrite lineSep buffersets task-monitor memory-status ml-status errors clock
+view.status=( mode , fold , encoding ) locked wrap multiSelect rectSelect overwrite lineSep buffersets task-monitor java-status ml-status errors clock
view.thickCaret=true
view.width=1200
xml-insert-closing-tag.shortcut=
--- a/src/Tools/jEdit/src/services.xml Thu Sep 10 16:04:12 2020 +0200
+++ b/src/Tools/jEdit/src/services.xml Thu Sep 10 21:07:58 2020 +0200
@@ -50,6 +50,9 @@
<SERVICE CLASS="isabelle.jedit.Active$Handler" NAME="graphview">
new isabelle.jedit.Graphview_Dockable$Handler()
</SERVICE>
+ <SERVICE CLASS="org.gjt.sp.jedit.gui.statusbar.StatusWidgetFactory" NAME="java-status">
+ new isabelle.jedit.Status_Widget$Java_Factory();
+ </SERVICE>
<SERVICE CLASS="org.gjt.sp.jedit.gui.statusbar.StatusWidgetFactory" NAME="ml-status">
new isabelle.jedit.Status_Widget$ML_Factory();
</SERVICE>
--- a/src/Tools/jEdit/src/status_widget.scala Thu Sep 10 16:04:12 2020 +0200
+++ b/src/Tools/jEdit/src/status_widget.scala Thu Sep 10 21:07:58 2020 +0200
@@ -8,31 +8,26 @@
import isabelle._
-
import java.awt.{Color, Dimension, Graphics, Graphics2D, Insets, RenderingHints}
import java.awt.font.FontRenderContext
-import java.awt.event.{MouseAdapter, MouseEvent}
-import javax.swing.{JComponent, JLabel}
+import java.awt.event.{ActionEvent, ActionListener, MouseAdapter, MouseEvent}
+import javax.swing.{JComponent, JLabel, Timer}
import org.gjt.sp.jedit.{View, jEdit}
import org.gjt.sp.jedit.gui.statusbar.{StatusWidgetFactory, Widget}
object Status_Widget
{
- private val template = "99999/99999MB"
+ /** generic GUI **/
- private class GUI(view: View) extends JComponent
+ private val template = "ABC: 99999/99999MB"
+
+ abstract class GUI(view: View) extends JComponent
{
- /* component state -- owned by GUI thread */
-
- private var status = ML_Statistics.memory_status(Nil)
-
-
/* init */
setFont(new JLabel().getFont)
- setToolTipText("ML heap memory (double-click for monitor panel)")
private val font_render_context = new FontRenderContext(null, true, false)
private val line_metrics = getFont.getLineMetrics(template, font_render_context)
@@ -53,13 +48,7 @@
/* paint */
- private def update(new_status: ML_Statistics.Memory_Status)
- {
- if (status != new_status) {
- status = new_status
- repaint()
- }
- }
+ def get_status: (String, Double)
override def paintComponent(gfx: Graphics)
{
@@ -70,14 +59,7 @@
val width = getWidth - insets.left - insets.right
val height = getHeight - insets.top - insets.bottom - 1
- val (text, fraction) =
- status.gc_progress match {
- case Some(p) => ("ML cleanup", 1.0 - p)
- case None =>
- ((status.heap_used / 1024 / 1024) + "/" + (status.heap_size / 1024 / 1024) + "MB",
- status.heap_used_fraction)
- }
-
+ val (text, fraction) = get_status
val width2 = (width * fraction).toInt
val text_bounds = gfx.getFont.getStringBounds(text, font_render_context)
@@ -102,13 +84,114 @@
}
+ /* mouse listener */
+
+ def action: String
+
+ addMouseListener(new MouseAdapter {
+ override def mouseClicked(evt: MouseEvent)
+ {
+ if (evt.getClickCount == 2) {
+ view.getInputHandler.invokeAction(action)
+ }
+ }
+ })
+ }
+
+
+
+ /** Java **/
+
+ class Java_GUI(view: View) extends GUI(view)
+ {
+ /* component state -- owned by GUI thread */
+
+ private var status = Platform.memory_status()
+
+ def get_status: (String, Double) =
+ {
+ ("JVM: " + (status.heap_used / 1024 / 1024) + "/" + (status.heap_size / 1024 / 1024) + "MB",
+ status.heap_used_fraction)
+ }
+
+ private def update_status(new_status: Platform.Memory_Status)
+ {
+ if (status != new_status) {
+ status = new_status
+ repaint()
+ }
+ }
+
+
+ /* timer */
+
+ private val timer =
+ new Timer(500, new ActionListener {
+ override def actionPerformed(e: ActionEvent) {
+ update_status(Platform.memory_status())
+ }
+ })
+
+ override def addNotify()
+ {
+ super.addNotify()
+ timer.start()
+ }
+
+ override def removeNotify()
+ {
+ super.removeNotify()
+ timer.stop()
+ }
+
+
+ /* action */
+
+ setToolTipText("Java heap memory (double-click for monitor application)")
+
+ override def action: String = "isabelle.jconsole"
+ }
+
+ class Java_Factory extends StatusWidgetFactory
+ {
+ override def getWidget(view: View): Widget =
+ new Widget { override def getComponent: JComponent = new Java_GUI(view) }
+ }
+
+
+
+ /** ML **/
+
+ class ML_GUI(view: View) extends GUI(view)
+ {
+ /* component state -- owned by GUI thread */
+
+ private var status = ML_Statistics.memory_status(Nil)
+
+ def get_status: (String, Double) =
+ status.gc_progress match {
+ case Some(p) => ("ML cleanup", 1.0 - p)
+ case None =>
+ ("ML: " + (status.heap_used / 1024 / 1024) + "/" + (status.heap_size / 1024 / 1024) + "MB",
+ status.heap_used_fraction)
+ }
+
+ private def update_status(new_status: ML_Statistics.Memory_Status)
+ {
+ if (status != new_status) {
+ status = new_status
+ repaint()
+ }
+ }
+
+
/* main */
private val main =
Session.Consumer[Session.Runtime_Statistics](getClass.getName) {
case stats =>
val status = ML_Statistics.memory_status(stats.props)
- GUI_Thread.later { update(status) }
+ GUI_Thread.later { update_status(status) }
}
override def addNotify()
@@ -124,21 +207,16 @@
}
- /* mouse listener */
+ /* action */
- addMouseListener(new MouseAdapter {
- override def mouseClicked(evt: MouseEvent)
- {
- if (evt.getClickCount == 2) {
- view.getInputHandler.invokeAction("isabelle-monitor-float")
- }
- }
- })
+ setToolTipText("ML heap memory (double-click for monitor panel)")
+
+ override def action: String = "isabelle-monitor-float"
}
class ML_Factory extends StatusWidgetFactory
{
override def getWidget(view: View): Widget =
- new Widget { override def getComponent: JComponent = new GUI(view) }
+ new Widget { override def getComponent: JComponent = new ML_GUI(view) }
}
}