--- 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"
--- 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) }
- }
-}
--- 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()
</SERVICE>
<SERVICE CLASS="org.gjt.sp.jedit.gui.statusbar.StatusWidgetFactory" NAME="ml-status">
- new isabelle.jedit.ML_Status$Widget_Factory();
+ new isabelle.jedit.Status_Widget$ML_Factory();
</SERVICE>
</SERVICES>
--- /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) }
+ }
+}