ML status widget similar to org.gjt.sp.jedit.gui.statusbar.MemoryStatusWidgetFactory;

--- a/src/Tools/jEdit/lib/Tools/jedit	Wed Aug 12 19:32:45 2020 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Aug 12 19:34:38 2020 +0200
@@ -49,6 +49,7 @@
   "src/Tools/jEdit/src/jedit_sessions.scala"
   "src/Tools/jEdit/src/jedit_spell_checker.scala"
   "src/Tools/jEdit/src/keymap_merge.scala"
+  "src/Tools/jEdit/src/ml_status.scala"
   "src/Tools/jEdit/src/monitor_dockable.scala"
   "src/Tools/jEdit/src/output_dockable.scala"
   "src/Tools/jEdit/src/plugin.scala"

--- a/src/Tools/jEdit/src/jEdit.props	Wed Aug 12 19:32:45 2020 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Wed Aug 12 19:34:38 2020 +0200
@@ -337,6 +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.thickCaret=true
 view.width=1200
 xml-insert-closing-tag.shortcut=

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/ml_status.scala	Wed Aug 12 19:34:38 2020 +0200
@@ -0,0 +1,124 @@
+/*  Title:      Tools/jEdit/src/ml_status.scala
+    Author:     Makarius
+
+ML status bar: heap and garbage collection.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.{Color, Dimension, Graphics, Graphics2D, Insets, RenderingHints}
+import java.awt.font.FontRenderContext
+import javax.swing.{JComponent, JLabel}
+
+import org.gjt.sp.jedit.{View, jEdit}
+import org.gjt.sp.jedit.gui.statusbar.{StatusWidgetFactory, Widget}
+
+
+object ML_Status
+{
+  private val template = "99999/99999MB"
+
+  private class GUI 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")
+
+    private val font_render_context = new FontRenderContext(null, true, false)
+    private val line_metrics = getFont.getLineMetrics(template, font_render_context)
+
+    {
+      val bounds = getFont.getStringBounds(template, font_render_context)
+      val dim = new Dimension(bounds.getWidth.toInt, bounds.getHeight.toInt)
+      setPreferredSize(dim)
+      setMaximumSize(dim)
+    }
+
+    setForeground(jEdit.getColorProperty("view.status.foreground"))
+    setBackground(jEdit.getColorProperty("view.status.background"))
+
+    def progress_foreground: Color = jEdit.getColorProperty("view.status.memory.foreground")
+    def progress_background: Color = jEdit.getColorProperty("view.status.memory.background")
+
+
+    /* paint */
+
+    private def update(new_status: ML_Statistics.Memory_Status)
+    {
+      if (status != new_status) {
+        status = new_status
+        repaint()
+      }
+    }
+
+    override def paintComponent(gfx: Graphics)
+    {
+      super.paintComponent(gfx)
+
+      val insets = new Insets(0, 0, 0, 0)
+
+      val width = getWidth - insets.left - insets.right
+      val height = getHeight - insets.top - insets.bottom - 1
+
+      val width_used = (width * status.heap_used_fraction).toInt
+
+      val text = (status.heap_used / 1024 / 1024) + "/" + (status.heap_size / 1024 / 1024) + "MB"
+      val text_bounds = gfx.getFont.getStringBounds(text, font_render_context)
+      val text_x = insets.left + ((width - text_bounds.getWidth).toInt / 2)
+      val text_y = (insets.top + line_metrics.getAscent).toInt
+
+      gfx.asInstanceOf[Graphics2D].
+        setRenderingHint(
+          RenderingHints.KEY_TEXT_ANTIALIASING,
+          RenderingHints.VALUE_TEXT_ANTIALIAS_ON)
+
+      gfx.setColor(progress_background)
+      gfx.fillRect(insets.left, insets.top, width_used, height)
+
+      gfx.setColor(progress_foreground)
+      gfx.setClip(insets.left, insets.top, width_used, height)
+      gfx.drawString(text, text_x, text_y)
+
+      gfx.setColor(getForeground)
+      gfx.setClip(insets.left + width_used, insets.top, getWidth - insets.left - width_used, height)
+      gfx.drawString(text, text_x, text_y)
+    }
+
+
+    /* 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) }
+      }
+
+    override def addNotify()
+    {
+      super.addNotify()
+      PIDE.session.runtime_statistics += main
+    }
+
+    override def removeNotify()
+    {
+      super.removeNotify()
+      PIDE.session.runtime_statistics -= main
+    }
+  }
+
+  class Widget_Factory extends StatusWidgetFactory
+  {
+    override def getWidget(view: View): Widget =
+      new Widget { override def getComponent: JComponent = new GUI }
+  }
+}

--- a/src/Tools/jEdit/src/services.xml	Wed Aug 12 19:32:45 2020 +0200
+++ b/src/Tools/jEdit/src/services.xml	Wed Aug 12 19:34:38 2020 +0200
@@ -50,4 +50,7 @@
   <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="ml-status">
+		new isabelle.jedit.ML_Status$Widget_Factory();
+	</SERVICE>
 </SERVICES>