# HG changeset patch # User wenzelm # Date 1597253678 -7200 # Node ID f5c085dfa02f9646a9e954adb1fe7386c7675acb # Parent fa57d299b46b3c08a09940daeb94d9493b525789 ML status widget similar to org.gjt.sp.jedit.gui.statusbar.MemoryStatusWidgetFactory; diff -r fa57d299b46b -r f5c085dfa02f src/Tools/jEdit/lib/Tools/jedit --- 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" diff -r fa57d299b46b -r f5c085dfa02f src/Tools/jEdit/src/jEdit.props --- 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= diff -r fa57d299b46b -r f5c085dfa02f src/Tools/jEdit/src/ml_status.scala --- /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 } + } +} diff -r fa57d299b46b -r f5c085dfa02f src/Tools/jEdit/src/services.xml --- 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 @@ new isabelle.jedit.Graphview_Dockable$Handler() + + new isabelle.jedit.ML_Status$Widget_Factory(); +