# HG changeset patch # User wenzelm # Date 1599746652 -7200 # Node ID 71378e7d148e7c0e035d9b4ba28887a9567ec2c3 # Parent c06260b7152c8f10f5710e6273c28a13edf17c16 clarified modules; diff -r c06260b7152c -r 71378e7d148e src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Tue Sep 08 21:14:42 2020 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Thu Sep 10 16:04:12 2020 +0200 @@ -49,7 +49,6 @@ "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" @@ -66,6 +65,7 @@ "src/Tools/jEdit/src/simplifier_trace_window.scala" "src/Tools/jEdit/src/sledgehammer_dockable.scala" "src/Tools/jEdit/src/state_dockable.scala" + "src/Tools/jEdit/src/status_widget.scala" "src/Tools/jEdit/src/symbols_dockable.scala" "src/Tools/jEdit/src/syntax_style.scala" "src/Tools/jEdit/src/syslog_dockable.scala" diff -r c06260b7152c -r 71378e7d148e src/Tools/jEdit/src/ml_status.scala --- a/src/Tools/jEdit/src/ml_status.scala Tue Sep 08 21:14:42 2020 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,144 +0,0 @@ -/* 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 java.awt.event.{MouseAdapter, MouseEvent} -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(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) - - { - 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 (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 width2 = (width * fraction).toInt - - 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, width2, height) - - gfx.setColor(progress_foreground) - gfx.setClip(insets.left, insets.top, width2, height) - gfx.drawString(text, text_x, text_y) - - gfx.setColor(getForeground) - gfx.setClip(insets.left + width2, insets.top, getWidth - insets.left - width2, 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 - } - - - /* mouse listener */ - - addMouseListener(new MouseAdapter { - override def mouseClicked(evt: MouseEvent) - { - if (evt.getClickCount == 2) { - view.getInputHandler.invokeAction("isabelle-monitor-float") - } - } - }) - } - - class Widget_Factory extends StatusWidgetFactory - { - override def getWidget(view: View): Widget = - new Widget { override def getComponent: JComponent = new GUI(view) } - } -} diff -r c06260b7152c -r 71378e7d148e src/Tools/jEdit/src/services.xml --- a/src/Tools/jEdit/src/services.xml Tue Sep 08 21:14:42 2020 +0200 +++ b/src/Tools/jEdit/src/services.xml Thu Sep 10 16:04:12 2020 +0200 @@ -51,6 +51,6 @@ new isabelle.jedit.Graphview_Dockable$Handler() - new isabelle.jedit.ML_Status$Widget_Factory(); + new isabelle.jedit.Status_Widget$ML_Factory(); diff -r c06260b7152c -r 71378e7d148e src/Tools/jEdit/src/status_widget.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/status_widget.scala Thu Sep 10 16:04:12 2020 +0200 @@ -0,0 +1,144 @@ +/* Title: Tools/jEdit/src/status_widget.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 java.awt.event.{MouseAdapter, MouseEvent} +import javax.swing.{JComponent, JLabel} + +import org.gjt.sp.jedit.{View, jEdit} +import org.gjt.sp.jedit.gui.statusbar.{StatusWidgetFactory, Widget} + + +object Status_Widget +{ + private val template = "99999/99999MB" + + private 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) + + { + 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 (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 width2 = (width * fraction).toInt + + 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, width2, height) + + gfx.setColor(progress_foreground) + gfx.setClip(insets.left, insets.top, width2, height) + gfx.drawString(text, text_x, text_y) + + gfx.setColor(getForeground) + gfx.setClip(insets.left + width2, insets.top, getWidth - insets.left - width2, 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 + } + + + /* mouse listener */ + + addMouseListener(new MouseAdapter { + override def mouseClicked(evt: MouseEvent) + { + if (evt.getClickCount == 2) { + view.getInputHandler.invokeAction("isabelle-monitor-float") + } + } + }) + } + + class ML_Factory extends StatusWidgetFactory + { + override def getWidget(view: View): Widget = + new Widget { override def getComponent: JComponent = new GUI(view) } + } +}